Database
ZF (ZERMELO-FRAENKEL) SET THEORY
ZF Set Theory - add the Axiom of Power Sets
Definite description binder (inverted iota)
iotauni2
Next ⟩
iotanul2
Metamath Proof Explorer
Ascii
Unicode
Theorem
iotauni2
Description:
Version of
iotauni
using
df-iota
instead of
dfiota2
.
(Contributed by
SN
, 6-Nov-2024)
Ref
Expression
Assertion
iotauni2
⊢
∃
y
x
|
φ
=
y
→
ι
x
|
φ
=
⋃
x
|
φ
Proof
Step
Hyp
Ref
Expression
1
iotaval2
⊢
x
|
φ
=
y
→
ι
x
|
φ
=
y
2
unieq
⊢
x
|
φ
=
y
→
⋃
x
|
φ
=
⋃
y
3
unisnv
⊢
⋃
y
=
y
4
2
3
eqtr2di
⊢
x
|
φ
=
y
→
y
=
⋃
x
|
φ
5
1
4
eqtrd
⊢
x
|
φ
=
y
→
ι
x
|
φ
=
⋃
x
|
φ
6
5
exlimiv
⊢
∃
y
x
|
φ
=
y
→
ι
x
|
φ
=
⋃
x
|
φ