Metamath Proof Explorer


Theorem opabex3d

Description: Existence of an ordered pair abstraction, deduction version. (Contributed by Alexander van der Vekens, 19-Oct-2017) (Revised by AV, 9-Aug-2024)

Ref Expression
Hypotheses opabex3d.1 ( 𝜑𝐴𝑉 )
opabex3d.2 ( ( 𝜑𝑥𝐴 ) → { 𝑦𝜓 } ∈ V )
Assertion opabex3d ( 𝜑 → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥𝐴𝜓 ) } ∈ V )

Proof

Step Hyp Ref Expression
1 opabex3d.1 ( 𝜑𝐴𝑉 )
2 opabex3d.2 ( ( 𝜑𝑥𝐴 ) → { 𝑦𝜓 } ∈ V )
3 19.42v ( ∃ 𝑦 ( 𝑥𝐴 ∧ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜓 ) ) ↔ ( 𝑥𝐴 ∧ ∃ 𝑦 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜓 ) ) )
4 an12 ( ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑥𝐴𝜓 ) ) ↔ ( 𝑥𝐴 ∧ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜓 ) ) )
5 4 exbii ( ∃ 𝑦 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑥𝐴𝜓 ) ) ↔ ∃ 𝑦 ( 𝑥𝐴 ∧ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜓 ) ) )
6 elxp ( 𝑧 ∈ ( { 𝑥 } × { 𝑦𝜓 } ) ↔ ∃ 𝑣𝑤 ( 𝑧 = ⟨ 𝑣 , 𝑤 ⟩ ∧ ( 𝑣 ∈ { 𝑥 } ∧ 𝑤 ∈ { 𝑦𝜓 } ) ) )
7 excom ( ∃ 𝑣𝑤 ( 𝑧 = ⟨ 𝑣 , 𝑤 ⟩ ∧ ( 𝑣 ∈ { 𝑥 } ∧ 𝑤 ∈ { 𝑦𝜓 } ) ) ↔ ∃ 𝑤𝑣 ( 𝑧 = ⟨ 𝑣 , 𝑤 ⟩ ∧ ( 𝑣 ∈ { 𝑥 } ∧ 𝑤 ∈ { 𝑦𝜓 } ) ) )
8 an12 ( ( 𝑧 = ⟨ 𝑣 , 𝑤 ⟩ ∧ ( 𝑣 ∈ { 𝑥 } ∧ 𝑤 ∈ { 𝑦𝜓 } ) ) ↔ ( 𝑣 ∈ { 𝑥 } ∧ ( 𝑧 = ⟨ 𝑣 , 𝑤 ⟩ ∧ 𝑤 ∈ { 𝑦𝜓 } ) ) )
9 velsn ( 𝑣 ∈ { 𝑥 } ↔ 𝑣 = 𝑥 )
10 9 anbi1i ( ( 𝑣 ∈ { 𝑥 } ∧ ( 𝑧 = ⟨ 𝑣 , 𝑤 ⟩ ∧ 𝑤 ∈ { 𝑦𝜓 } ) ) ↔ ( 𝑣 = 𝑥 ∧ ( 𝑧 = ⟨ 𝑣 , 𝑤 ⟩ ∧ 𝑤 ∈ { 𝑦𝜓 } ) ) )
11 8 10 bitri ( ( 𝑧 = ⟨ 𝑣 , 𝑤 ⟩ ∧ ( 𝑣 ∈ { 𝑥 } ∧ 𝑤 ∈ { 𝑦𝜓 } ) ) ↔ ( 𝑣 = 𝑥 ∧ ( 𝑧 = ⟨ 𝑣 , 𝑤 ⟩ ∧ 𝑤 ∈ { 𝑦𝜓 } ) ) )
12 11 exbii ( ∃ 𝑣 ( 𝑧 = ⟨ 𝑣 , 𝑤 ⟩ ∧ ( 𝑣 ∈ { 𝑥 } ∧ 𝑤 ∈ { 𝑦𝜓 } ) ) ↔ ∃ 𝑣 ( 𝑣 = 𝑥 ∧ ( 𝑧 = ⟨ 𝑣 , 𝑤 ⟩ ∧ 𝑤 ∈ { 𝑦𝜓 } ) ) )
13 opeq1 ( 𝑣 = 𝑥 → ⟨ 𝑣 , 𝑤 ⟩ = ⟨ 𝑥 , 𝑤 ⟩ )
14 13 eqeq2d ( 𝑣 = 𝑥 → ( 𝑧 = ⟨ 𝑣 , 𝑤 ⟩ ↔ 𝑧 = ⟨ 𝑥 , 𝑤 ⟩ ) )
15 14 anbi1d ( 𝑣 = 𝑥 → ( ( 𝑧 = ⟨ 𝑣 , 𝑤 ⟩ ∧ 𝑤 ∈ { 𝑦𝜓 } ) ↔ ( 𝑧 = ⟨ 𝑥 , 𝑤 ⟩ ∧ 𝑤 ∈ { 𝑦𝜓 } ) ) )
16 15 equsexvw ( ∃ 𝑣 ( 𝑣 = 𝑥 ∧ ( 𝑧 = ⟨ 𝑣 , 𝑤 ⟩ ∧ 𝑤 ∈ { 𝑦𝜓 } ) ) ↔ ( 𝑧 = ⟨ 𝑥 , 𝑤 ⟩ ∧ 𝑤 ∈ { 𝑦𝜓 } ) )
17 12 16 bitri ( ∃ 𝑣 ( 𝑧 = ⟨ 𝑣 , 𝑤 ⟩ ∧ ( 𝑣 ∈ { 𝑥 } ∧ 𝑤 ∈ { 𝑦𝜓 } ) ) ↔ ( 𝑧 = ⟨ 𝑥 , 𝑤 ⟩ ∧ 𝑤 ∈ { 𝑦𝜓 } ) )
18 17 exbii ( ∃ 𝑤𝑣 ( 𝑧 = ⟨ 𝑣 , 𝑤 ⟩ ∧ ( 𝑣 ∈ { 𝑥 } ∧ 𝑤 ∈ { 𝑦𝜓 } ) ) ↔ ∃ 𝑤 ( 𝑧 = ⟨ 𝑥 , 𝑤 ⟩ ∧ 𝑤 ∈ { 𝑦𝜓 } ) )
19 7 18 bitri ( ∃ 𝑣𝑤 ( 𝑧 = ⟨ 𝑣 , 𝑤 ⟩ ∧ ( 𝑣 ∈ { 𝑥 } ∧ 𝑤 ∈ { 𝑦𝜓 } ) ) ↔ ∃ 𝑤 ( 𝑧 = ⟨ 𝑥 , 𝑤 ⟩ ∧ 𝑤 ∈ { 𝑦𝜓 } ) )
20 nfv 𝑦 𝑧 = ⟨ 𝑥 , 𝑤
21 nfsab1 𝑦 𝑤 ∈ { 𝑦𝜓 }
22 20 21 nfan 𝑦 ( 𝑧 = ⟨ 𝑥 , 𝑤 ⟩ ∧ 𝑤 ∈ { 𝑦𝜓 } )
23 nfv 𝑤 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜓 )
24 opeq2 ( 𝑤 = 𝑦 → ⟨ 𝑥 , 𝑤 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ )
25 24 eqeq2d ( 𝑤 = 𝑦 → ( 𝑧 = ⟨ 𝑥 , 𝑤 ⟩ ↔ 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ) )
26 df-clab ( 𝑤 ∈ { 𝑦𝜓 } ↔ [ 𝑤 / 𝑦 ] 𝜓 )
27 sbequ12 ( 𝑦 = 𝑤 → ( 𝜓 ↔ [ 𝑤 / 𝑦 ] 𝜓 ) )
28 27 equcoms ( 𝑤 = 𝑦 → ( 𝜓 ↔ [ 𝑤 / 𝑦 ] 𝜓 ) )
29 26 28 bitr4id ( 𝑤 = 𝑦 → ( 𝑤 ∈ { 𝑦𝜓 } ↔ 𝜓 ) )
30 25 29 anbi12d ( 𝑤 = 𝑦 → ( ( 𝑧 = ⟨ 𝑥 , 𝑤 ⟩ ∧ 𝑤 ∈ { 𝑦𝜓 } ) ↔ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜓 ) ) )
31 22 23 30 cbvexv1 ( ∃ 𝑤 ( 𝑧 = ⟨ 𝑥 , 𝑤 ⟩ ∧ 𝑤 ∈ { 𝑦𝜓 } ) ↔ ∃ 𝑦 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜓 ) )
32 6 19 31 3bitri ( 𝑧 ∈ ( { 𝑥 } × { 𝑦𝜓 } ) ↔ ∃ 𝑦 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜓 ) )
33 32 anbi2i ( ( 𝑥𝐴𝑧 ∈ ( { 𝑥 } × { 𝑦𝜓 } ) ) ↔ ( 𝑥𝐴 ∧ ∃ 𝑦 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜓 ) ) )
34 3 5 33 3bitr4ri ( ( 𝑥𝐴𝑧 ∈ ( { 𝑥 } × { 𝑦𝜓 } ) ) ↔ ∃ 𝑦 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑥𝐴𝜓 ) ) )
35 34 exbii ( ∃ 𝑥 ( 𝑥𝐴𝑧 ∈ ( { 𝑥 } × { 𝑦𝜓 } ) ) ↔ ∃ 𝑥𝑦 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑥𝐴𝜓 ) ) )
36 eliun ( 𝑧 𝑥𝐴 ( { 𝑥 } × { 𝑦𝜓 } ) ↔ ∃ 𝑥𝐴 𝑧 ∈ ( { 𝑥 } × { 𝑦𝜓 } ) )
37 df-rex ( ∃ 𝑥𝐴 𝑧 ∈ ( { 𝑥 } × { 𝑦𝜓 } ) ↔ ∃ 𝑥 ( 𝑥𝐴𝑧 ∈ ( { 𝑥 } × { 𝑦𝜓 } ) ) )
38 36 37 bitri ( 𝑧 𝑥𝐴 ( { 𝑥 } × { 𝑦𝜓 } ) ↔ ∃ 𝑥 ( 𝑥𝐴𝑧 ∈ ( { 𝑥 } × { 𝑦𝜓 } ) ) )
39 elopab ( 𝑧 ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥𝐴𝜓 ) } ↔ ∃ 𝑥𝑦 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑥𝐴𝜓 ) ) )
40 35 38 39 3bitr4i ( 𝑧 𝑥𝐴 ( { 𝑥 } × { 𝑦𝜓 } ) ↔ 𝑧 ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥𝐴𝜓 ) } )
41 40 eqriv 𝑥𝐴 ( { 𝑥 } × { 𝑦𝜓 } ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥𝐴𝜓 ) }
42 snex { 𝑥 } ∈ V
43 xpexg ( ( { 𝑥 } ∈ V ∧ { 𝑦𝜓 } ∈ V ) → ( { 𝑥 } × { 𝑦𝜓 } ) ∈ V )
44 42 2 43 sylancr ( ( 𝜑𝑥𝐴 ) → ( { 𝑥 } × { 𝑦𝜓 } ) ∈ V )
45 44 ralrimiva ( 𝜑 → ∀ 𝑥𝐴 ( { 𝑥 } × { 𝑦𝜓 } ) ∈ V )
46 iunexg ( ( 𝐴𝑉 ∧ ∀ 𝑥𝐴 ( { 𝑥 } × { 𝑦𝜓 } ) ∈ V ) → 𝑥𝐴 ( { 𝑥 } × { 𝑦𝜓 } ) ∈ V )
47 1 45 46 syl2anc ( 𝜑 𝑥𝐴 ( { 𝑥 } × { 𝑦𝜓 } ) ∈ V )
48 41 47 eqeltrrid ( 𝜑 → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥𝐴𝜓 ) } ∈ V )