[EricSchmidt-119]

Revise iotan0 to remove sethood requirement.

Theorem sgrpidmnd was revised to use the new version.

[benjub]

Suggested change

	Remove sethood requirement from antecedent. (Revised by Eric Schmidt,
	17-Oct-2026.) $)
	Remove sethood antecedent. (Revised by Eric Schmidt, 17-Oct-2026.) $)

Slightly less explicit, but more compact, and set.mm already has many mentions of "sethood antecedent/hypothesis" (not only by me!) as an acceptable shortening for "sethood condition in antecedent/hypthesis".

Side note: with the definition https://us.metamath.org/mpeuni/df-aiota.html, it is the non-emptiness antecedent which is superfluous, while the "existence" of A as a set remains necessary. That gives a more natural statement, closer to statements like spcgf. I will probably add that small remark to the comment of df-aiota. FYI @avekens

[avekens]

The following corresponding theorem can be proven for my alternate definition of iota:

  ${
    $d A x $.  $d ps x $.
    aiotaex.1 $e |- ( x = A -> ( ph <-> ps ) ) $.
    $( Representation of "the unique element such that ` ph ` " with a class
       expression ` A ` which is a set (that means that "the unique element
	   such that ` ph ` " exists).  (Contributed by AV, 18-Oct-2026.) $)
    aiotaex $p |- ( ( A e. V /\ A = ( iota' x ph ) ) -> ps ) $=
      ( caiota wceq wcel weu cab cint cvv cif wi dfaiota3 eqeq2i iftrue eqeq2d
      sylbid cio iotain eqcom wa iota2 biimprd expcom com23 biimtrid wn iffalse
      nvelim pm2.21d a1i pm2.61i sylbi impcom ) DACGZHZDEIZBUSDACJZACKLZMNZHZUT
      BOZURVCDACPQVAVDVEOVAVDDVBHZVEVAVCVBDVAVBMRSVAVFDACUAZHZVEVAVBVGDACUBSVHV
      GDHZVAVEDVGUCVAUTVIBUTVAVIBOUTVAUDBVIABCDEFUEUFUGUHUITTVAUJZVDDMHZVEVJVCM
      DVAVBMUKSVKVEOVJVKUTBDEULUMUNTUOUPUQ $.
  $}

This can be added (maybe with a separate PR) to my mathbox.

[EricSchmidt-119]

@avekens I think it would make sense for you to add that yourself in a different PR.

[benjub]

Yes, that's the statement I had in mind. Indeed, it can be added in a future PR: I didn't mean with my "side note" to block this PR.

[avekens]

The following corresponding theorem can be proven for my alternate definition of iota:

  ${
    $d A x $.  $d ps x $.
    aiotaex.1 $e |- ( x = A -> ( ph <-> ps ) ) $.
    $( Representation of "the unique element such that ` ph ` " with a class
       expression ` A ` which is a set (that means that "the unique element
	   such that ` ph ` " exists).  (Contributed by AV, 18-Oct-2026.) $)
    aiotaex $p |- ( ( A e. V /\ A = ( iota' x ph ) ) -> ps ) $=
      ( caiota wceq wcel weu cab cint cvv cif wi dfaiota3 eqeq2i iftrue eqeq2d
      sylbid cio iotain eqcom wa iota2 biimprd expcom com23 biimtrid wn iffalse
      nvelim pm2.21d a1i pm2.61i sylbi impcom ) DACGZHZDEIZBUSDACJZACKLZMNZHZUT
      BOZURVCDACPQVAVDVEOVAVDDVBHZVEVAVCVBDVAVBMRSVAVFDACUAZHZVEVAVBVGDACUBSVHV
      GDHZVAVEDVGUCVAUTVIBUTVAVIBOUTVAUDBVIABCDEFUEUFUGUHUITTVAUJZVDDMHZVEVJVCM
      DVAVBMUKSVKVEOVJVKUTBDEULUMUNTUOUPUQ $.
  $}

This can be added (maybe with a separate PR) to my mathbox.

To be precise: This is not "my alternate definition of iota", but it is "the alternate definition df-aiota", which was proposed by @benjub and we worked with it in a collaborative way in my mathbox.

I'll add ~aiotaex to my mathbox in a subsequent PR.