Metamath Proof Explorer


Theorem dfiota3

Description: A definition of iota using minimal quantifiers. (Contributed by Scott Fenton, 19-Feb-2013)

Ref Expression
Assertion dfiota3 ( ℩ 𝑥 𝜑 ) = ( { { 𝑥𝜑 } } ∩ Singletons )

Proof

Step Hyp Ref Expression
1 df-iota ( ℩ 𝑥 𝜑 ) = { 𝑦 ∣ { 𝑥𝜑 } = { 𝑦 } }
2 abeq1 ( { 𝑦 ∣ { 𝑥𝜑 } = { 𝑦 } } = { 𝑧 ∣ ∃ 𝑤 ( 𝑧 = { 𝑥𝜑 } ∧ 𝑧 = { 𝑤 } ) } ↔ ∀ 𝑦 ( { 𝑥𝜑 } = { 𝑦 } ↔ 𝑦 { 𝑧 ∣ ∃ 𝑤 ( 𝑧 = { 𝑥𝜑 } ∧ 𝑧 = { 𝑤 } ) } ) )
3 exdistr ( ∃ 𝑧𝑤 ( 𝑦𝑧 ∧ ( 𝑧 = { 𝑥𝜑 } ∧ 𝑧 = { 𝑤 } ) ) ↔ ∃ 𝑧 ( 𝑦𝑧 ∧ ∃ 𝑤 ( 𝑧 = { 𝑥𝜑 } ∧ 𝑧 = { 𝑤 } ) ) )
4 vex 𝑦 ∈ V
5 sneq ( 𝑤 = 𝑦 → { 𝑤 } = { 𝑦 } )
6 5 eqeq2d ( 𝑤 = 𝑦 → ( { 𝑥𝜑 } = { 𝑤 } ↔ { 𝑥𝜑 } = { 𝑦 } ) )
7 4 6 ceqsexv ( ∃ 𝑤 ( 𝑤 = 𝑦 ∧ { 𝑥𝜑 } = { 𝑤 } ) ↔ { 𝑥𝜑 } = { 𝑦 } )
8 snex { 𝑤 } ∈ V
9 eqeq1 ( 𝑧 = { 𝑤 } → ( 𝑧 = { 𝑥𝜑 } ↔ { 𝑤 } = { 𝑥𝜑 } ) )
10 eleq2 ( 𝑧 = { 𝑤 } → ( 𝑦𝑧𝑦 ∈ { 𝑤 } ) )
11 9 10 anbi12d ( 𝑧 = { 𝑤 } → ( ( 𝑧 = { 𝑥𝜑 } ∧ 𝑦𝑧 ) ↔ ( { 𝑤 } = { 𝑥𝜑 } ∧ 𝑦 ∈ { 𝑤 } ) ) )
12 eqcom ( { 𝑤 } = { 𝑥𝜑 } ↔ { 𝑥𝜑 } = { 𝑤 } )
13 velsn ( 𝑦 ∈ { 𝑤 } ↔ 𝑦 = 𝑤 )
14 equcom ( 𝑦 = 𝑤𝑤 = 𝑦 )
15 13 14 bitri ( 𝑦 ∈ { 𝑤 } ↔ 𝑤 = 𝑦 )
16 12 15 anbi12ci ( ( { 𝑤 } = { 𝑥𝜑 } ∧ 𝑦 ∈ { 𝑤 } ) ↔ ( 𝑤 = 𝑦 ∧ { 𝑥𝜑 } = { 𝑤 } ) )
17 11 16 bitrdi ( 𝑧 = { 𝑤 } → ( ( 𝑧 = { 𝑥𝜑 } ∧ 𝑦𝑧 ) ↔ ( 𝑤 = 𝑦 ∧ { 𝑥𝜑 } = { 𝑤 } ) ) )
18 8 17 ceqsexv ( ∃ 𝑧 ( 𝑧 = { 𝑤 } ∧ ( 𝑧 = { 𝑥𝜑 } ∧ 𝑦𝑧 ) ) ↔ ( 𝑤 = 𝑦 ∧ { 𝑥𝜑 } = { 𝑤 } ) )
19 an13 ( ( 𝑧 = { 𝑤 } ∧ ( 𝑧 = { 𝑥𝜑 } ∧ 𝑦𝑧 ) ) ↔ ( 𝑦𝑧 ∧ ( 𝑧 = { 𝑥𝜑 } ∧ 𝑧 = { 𝑤 } ) ) )
20 19 exbii ( ∃ 𝑧 ( 𝑧 = { 𝑤 } ∧ ( 𝑧 = { 𝑥𝜑 } ∧ 𝑦𝑧 ) ) ↔ ∃ 𝑧 ( 𝑦𝑧 ∧ ( 𝑧 = { 𝑥𝜑 } ∧ 𝑧 = { 𝑤 } ) ) )
21 18 20 bitr3i ( ( 𝑤 = 𝑦 ∧ { 𝑥𝜑 } = { 𝑤 } ) ↔ ∃ 𝑧 ( 𝑦𝑧 ∧ ( 𝑧 = { 𝑥𝜑 } ∧ 𝑧 = { 𝑤 } ) ) )
22 21 exbii ( ∃ 𝑤 ( 𝑤 = 𝑦 ∧ { 𝑥𝜑 } = { 𝑤 } ) ↔ ∃ 𝑤𝑧 ( 𝑦𝑧 ∧ ( 𝑧 = { 𝑥𝜑 } ∧ 𝑧 = { 𝑤 } ) ) )
23 7 22 bitr3i ( { 𝑥𝜑 } = { 𝑦 } ↔ ∃ 𝑤𝑧 ( 𝑦𝑧 ∧ ( 𝑧 = { 𝑥𝜑 } ∧ 𝑧 = { 𝑤 } ) ) )
24 excom ( ∃ 𝑤𝑧 ( 𝑦𝑧 ∧ ( 𝑧 = { 𝑥𝜑 } ∧ 𝑧 = { 𝑤 } ) ) ↔ ∃ 𝑧𝑤 ( 𝑦𝑧 ∧ ( 𝑧 = { 𝑥𝜑 } ∧ 𝑧 = { 𝑤 } ) ) )
25 23 24 bitri ( { 𝑥𝜑 } = { 𝑦 } ↔ ∃ 𝑧𝑤 ( 𝑦𝑧 ∧ ( 𝑧 = { 𝑥𝜑 } ∧ 𝑧 = { 𝑤 } ) ) )
26 eluniab ( 𝑦 { 𝑧 ∣ ∃ 𝑤 ( 𝑧 = { 𝑥𝜑 } ∧ 𝑧 = { 𝑤 } ) } ↔ ∃ 𝑧 ( 𝑦𝑧 ∧ ∃ 𝑤 ( 𝑧 = { 𝑥𝜑 } ∧ 𝑧 = { 𝑤 } ) ) )
27 3 25 26 3bitr4i ( { 𝑥𝜑 } = { 𝑦 } ↔ 𝑦 { 𝑧 ∣ ∃ 𝑤 ( 𝑧 = { 𝑥𝜑 } ∧ 𝑧 = { 𝑤 } ) } )
28 2 27 mpgbir { 𝑦 ∣ { 𝑥𝜑 } = { 𝑦 } } = { 𝑧 ∣ ∃ 𝑤 ( 𝑧 = { 𝑥𝜑 } ∧ 𝑧 = { 𝑤 } ) }
29 df-sn { { 𝑥𝜑 } } = { 𝑧𝑧 = { 𝑥𝜑 } }
30 dfsingles2 Singletons = { 𝑧 ∣ ∃ 𝑤 𝑧 = { 𝑤 } }
31 29 30 ineq12i ( { { 𝑥𝜑 } } ∩ Singletons ) = ( { 𝑧𝑧 = { 𝑥𝜑 } } ∩ { 𝑧 ∣ ∃ 𝑤 𝑧 = { 𝑤 } } )
32 inab ( { 𝑧𝑧 = { 𝑥𝜑 } } ∩ { 𝑧 ∣ ∃ 𝑤 𝑧 = { 𝑤 } } ) = { 𝑧 ∣ ( 𝑧 = { 𝑥𝜑 } ∧ ∃ 𝑤 𝑧 = { 𝑤 } ) }
33 19.42v ( ∃ 𝑤 ( 𝑧 = { 𝑥𝜑 } ∧ 𝑧 = { 𝑤 } ) ↔ ( 𝑧 = { 𝑥𝜑 } ∧ ∃ 𝑤 𝑧 = { 𝑤 } ) )
34 33 bicomi ( ( 𝑧 = { 𝑥𝜑 } ∧ ∃ 𝑤 𝑧 = { 𝑤 } ) ↔ ∃ 𝑤 ( 𝑧 = { 𝑥𝜑 } ∧ 𝑧 = { 𝑤 } ) )
35 34 abbii { 𝑧 ∣ ( 𝑧 = { 𝑥𝜑 } ∧ ∃ 𝑤 𝑧 = { 𝑤 } ) } = { 𝑧 ∣ ∃ 𝑤 ( 𝑧 = { 𝑥𝜑 } ∧ 𝑧 = { 𝑤 } ) }
36 32 35 eqtri ( { 𝑧𝑧 = { 𝑥𝜑 } } ∩ { 𝑧 ∣ ∃ 𝑤 𝑧 = { 𝑤 } } ) = { 𝑧 ∣ ∃ 𝑤 ( 𝑧 = { 𝑥𝜑 } ∧ 𝑧 = { 𝑤 } ) }
37 31 36 eqtri ( { { 𝑥𝜑 } } ∩ Singletons ) = { 𝑧 ∣ ∃ 𝑤 ( 𝑧 = { 𝑥𝜑 } ∧ 𝑧 = { 𝑤 } ) }
38 37 unieqi ( { { 𝑥𝜑 } } ∩ Singletons ) = { 𝑧 ∣ ∃ 𝑤 ( 𝑧 = { 𝑥𝜑 } ∧ 𝑧 = { 𝑤 } ) }
39 28 38 eqtr4i { 𝑦 ∣ { 𝑥𝜑 } = { 𝑦 } } = ( { { 𝑥𝜑 } } ∩ Singletons )
40 39 unieqi { 𝑦 ∣ { 𝑥𝜑 } = { 𝑦 } } = ( { { 𝑥𝜑 } } ∩ Singletons )
41 1 40 eqtri ( ℩ 𝑥 𝜑 ) = ( { { 𝑥𝜑 } } ∩ Singletons )