Metamath Proof Explorer


Theorem dfiota3

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

Ref Expression
Assertion dfiota3 ι x | φ = x | φ 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇𝗌

Proof

Step Hyp Ref Expression
1 df-iota ι x | φ = y | x | φ = y
2 abeq1 y | x | φ = y = z | w z = x | φ z = w y x | φ = y y z | w z = x | φ z = w
3 exdistr z w y z z = x | φ z = w z y z w z = x | φ z = w
4 vex y V
5 sneq w = y w = y
6 5 eqeq2d w = y x | φ = w x | φ = y
7 4 6 ceqsexv w w = y x | φ = w x | φ = y
8 snex w V
9 eqeq1 z = w z = x | φ w = x | φ
10 eleq2 z = w y z y w
11 9 10 anbi12d z = w z = x | φ y z w = x | φ y w
12 eqcom w = x | φ x | φ = w
13 velsn y w y = w
14 equcom y = w w = y
15 13 14 bitri y w w = y
16 12 15 anbi12ci w = x | φ y w w = y x | φ = w
17 11 16 bitrdi z = w z = x | φ y z w = y x | φ = w
18 8 17 ceqsexv z z = w z = x | φ y z w = y x | φ = w
19 an13 z = w z = x | φ y z y z z = x | φ z = w
20 19 exbii z z = w z = x | φ y z z y z z = x | φ z = w
21 18 20 bitr3i w = y x | φ = w z y z z = x | φ z = w
22 21 exbii w w = y x | φ = w w z y z z = x | φ z = w
23 7 22 bitr3i x | φ = y w z y z z = x | φ z = w
24 excom w z y z z = x | φ z = w z w y z z = x | φ z = w
25 23 24 bitri x | φ = y z w y z z = x | φ z = w
26 eluniab y z | w z = x | φ z = w z y z w z = x | φ z = w
27 3 25 26 3bitr4i x | φ = y y z | w z = x | φ z = w
28 2 27 mpgbir y | x | φ = y = z | w z = x | φ z = w
29 df-sn x | φ = z | z = x | φ
30 dfsingles2 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇𝗌 = z | w z = w
31 29 30 ineq12i x | φ 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇𝗌 = z | z = x | φ z | w z = w
32 inab z | z = x | φ z | w z = w = z | z = x | φ w z = w
33 19.42v w z = x | φ z = w z = x | φ w z = w
34 33 bicomi z = x | φ w z = w w z = x | φ z = w
35 34 abbii z | z = x | φ w z = w = z | w z = x | φ z = w
36 32 35 eqtri z | z = x | φ z | w z = w = z | w z = x | φ z = w
37 31 36 eqtri x | φ 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇𝗌 = z | w z = x | φ z = w
38 37 unieqi x | φ 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇𝗌 = z | w z = x | φ z = w
39 28 38 eqtr4i y | x | φ = y = x | φ 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇𝗌
40 39 unieqi y | x | φ = y = x | φ 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇𝗌
41 1 40 eqtri ι x | φ = x | φ 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇𝗌