Metamath Proof Explorer


Theorem opabex3

Description: Existence of an ordered pair abstraction. (Contributed by Jeff Madsen, 2-Sep-2009)

Ref Expression
Hypotheses opabex3.1 A V
opabex3.2 x A y | φ V
Assertion opabex3 x y | x A φ V

Proof

Step Hyp Ref Expression
1 opabex3.1 A V
2 opabex3.2 x A y | φ V
3 19.42v y x A z = x y φ x A y z = x y φ
4 an12 z = x y x A φ x A z = x y φ
5 4 exbii y z = x y x A φ y x A z = x y φ
6 elxp z x × y | φ v w z = v w v x w y | φ
7 excom v w z = v w v x w y | φ w v z = v w v x w y | φ
8 an12 z = v w v x w y | φ v x z = v w w y | φ
9 velsn v x v = x
10 9 anbi1i v x z = v w w y | φ v = x z = v w w y | φ
11 8 10 bitri z = v w v x w y | φ v = x z = v w w y | φ
12 11 exbii v z = v w v x w y | φ v v = x z = v w w y | φ
13 opeq1 v = x v w = x w
14 13 eqeq2d v = x z = v w z = x w
15 14 anbi1d v = x z = v w w y | φ z = x w w y | φ
16 15 equsexvw v v = x z = v w w y | φ z = x w w y | φ
17 12 16 bitri v z = v w v x w y | φ z = x w w y | φ
18 17 exbii w v z = v w v x w y | φ w z = x w w y | φ
19 7 18 bitri v w z = v w v x w y | φ w z = x w w y | φ
20 nfv y z = x w
21 nfsab1 y w y | φ
22 20 21 nfan y z = x w w y | φ
23 nfv w z = x y φ
24 opeq2 w = y x w = x y
25 24 eqeq2d w = y z = x w z = x y
26 df-clab w y | φ w y φ
27 sbequ12 y = w φ w y φ
28 27 equcoms w = y φ w y φ
29 26 28 bitr4id w = y w y | φ φ
30 25 29 anbi12d w = y z = x w w y | φ z = x y φ
31 22 23 30 cbvexv1 w z = x w w y | φ y z = x y φ
32 6 19 31 3bitri z x × y | φ y z = x y φ
33 32 anbi2i x A z x × y | φ x A y z = x y φ
34 3 5 33 3bitr4ri x A z x × y | φ y z = x y x A φ
35 34 exbii x x A z x × y | φ x y z = x y x A φ
36 eliun z x A x × y | φ x A z x × y | φ
37 df-rex x A z x × y | φ x x A z x × y | φ
38 36 37 bitri z x A x × y | φ x x A z x × y | φ
39 elopab z x y | x A φ x y z = x y x A φ
40 35 38 39 3bitr4i z x A x × y | φ z x y | x A φ
41 40 eqriv x A x × y | φ = x y | x A φ
42 snex x V
43 xpexg x V y | φ V x × y | φ V
44 42 2 43 sylancr x A x × y | φ V
45 44 rgen x A x × y | φ V
46 iunexg A V x A x × y | φ V x A x × y | φ V
47 1 45 46 mp2an x A x × y | φ V
48 41 47 eqeltrri x y | x A φ V