Metamath Proof Explorer

Theorem iotavalOLD

Description: Obsolete version of iotaval as of 23-Dec-2024. (Contributed by Andrew Salmon, 11-Jul-2011) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion iotavalOLD ⊢∀xφ↔x=y→ιx|φ=y

Proof

Step Hyp Ref Expression
1 dfiota2 ⊢ιx|φ=⋃z|∀xφ↔x=z
2 sbeqalb ⊢y∈V→∀xφ↔x=y∧∀xφ↔x=z→y=z
3 2 elv ⊢∀xφ↔x=y∧∀xφ↔x=z→y=z
4 3 ex ⊢∀xφ↔x=y→∀xφ↔x=z→y=z
5 equequ2 ⊢y=z→x=y↔x=z
6 5 bibi2d ⊢y=z→φ↔x=y↔φ↔x=z
7 6 biimpd ⊢y=z→φ↔x=y→φ↔x=z
8 7 alimdv ⊢y=z→∀xφ↔x=y→∀xφ↔x=z
9 8 com12 ⊢∀xφ↔x=y→y=z→∀xφ↔x=z
10 4 9 impbid ⊢∀xφ↔x=y→∀xφ↔x=z↔y=z
11 equcom ⊢y=z↔z=y
12 10 11 bitrdi ⊢∀xφ↔x=y→∀xφ↔x=z↔z=y
13 12 alrimiv ⊢∀xφ↔x=y→∀z∀xφ↔x=z↔z=y
14 uniabio ⊢∀z∀xφ↔x=z↔z=y→⋃z|∀xφ↔x=z=y
15 13 14 syl ⊢∀xφ↔x=y→⋃z|∀xφ↔x=z=y
16 1 15 eqtrid ⊢∀xφ↔x=y→ιx|φ=y