Metamath Proof Explorer

Theorem reuop

Description: There is a unique ordered pair fulfilling a wff iff there are uniquely two sets fulfilling a corresponding wff. (Contributed by AV, 23-Jun-2023)

Ref Expression
Hypotheses reu3op.a ⊢ ( 𝑝 = ⟨ 𝑎 , 𝑏 ⟩ → ( 𝜓 ↔ 𝜒 ) )
reuop.x ⊢ ( 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝜓 ↔ 𝜃 ) )
Assertion reuop ( ∃! 𝑝 ∈ ( 𝑋 × 𝑌 ) 𝜓 ↔ ∃ 𝑎 ∈ 𝑋 ∃ 𝑏 ∈ 𝑌 ( 𝜒 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑌 ( 𝜃 → ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ) ) )

Proof

Step Hyp Ref Expression
1 reu3op.a ⊢ ( 𝑝 = ⟨ 𝑎 , 𝑏 ⟩ → ( 𝜓 ↔ 𝜒 ) )
2 reuop.x ⊢ ( 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝜓 ↔ 𝜃 ) )
3 nfsbc1v ⊢ Ⅎ 𝑝 [ 𝑞 / 𝑝 ] 𝜓
4 nfsbc1v ⊢ Ⅎ 𝑝 [ 𝑤 / 𝑝 ] 𝜓
5 sbceq1a ⊢ ( 𝑝 = 𝑤 → ( 𝜓 ↔ [ 𝑤 / 𝑝 ] 𝜓 ) )
6 dfsbcq ⊢ ( 𝑤 = 𝑞 → ( [ 𝑤 / 𝑝 ] 𝜓 ↔ [ 𝑞 / 𝑝 ] 𝜓 ) )
7 3 4 5 6 reu8nf ⊢ ( ∃! 𝑝 ∈ ( 𝑋 × 𝑌 ) 𝜓 ↔ ∃ 𝑝 ∈ ( 𝑋 × 𝑌 ) ( 𝜓 ∧ ∀ 𝑞 ∈ ( 𝑋 × 𝑌 ) ( [ 𝑞 / 𝑝 ] 𝜓 → 𝑝 = 𝑞 ) ) )
8 elxp2 ⊢ ( 𝑝 ∈ ( 𝑋 × 𝑌 ) ↔ ∃ 𝑎 ∈ 𝑋 ∃ 𝑏 ∈ 𝑌 𝑝 = ⟨ 𝑎 , 𝑏 ⟩ )
9 1 biimpcd ⊢ ( 𝜓 → ( 𝑝 = ⟨ 𝑎 , 𝑏 ⟩ → 𝜒 ) )
10 9 adantr ⊢ ( ( 𝜓 ∧ ∀ 𝑞 ∈ ( 𝑋 × 𝑌 ) ( [ 𝑞 / 𝑝 ] 𝜓 → 𝑝 = 𝑞 ) ) → ( 𝑝 = ⟨ 𝑎 , 𝑏 ⟩ → 𝜒 ) )
11 10 adantr ⊢ ( ( ( 𝜓 ∧ ∀ 𝑞 ∈ ( 𝑋 × 𝑌 ) ( [ 𝑞 / 𝑝 ] 𝜓 → 𝑝 = 𝑞 ) ) ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑌 ) ) → ( 𝑝 = ⟨ 𝑎 , 𝑏 ⟩ → 𝜒 ) )
12 11 imp ⊢ ( ( ( ( 𝜓 ∧ ∀ 𝑞 ∈ ( 𝑋 × 𝑌 ) ( [ 𝑞 / 𝑝 ] 𝜓 → 𝑝 = 𝑞 ) ) ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑌 ) ) ∧ 𝑝 = ⟨ 𝑎 , 𝑏 ⟩ ) → 𝜒 )
13 opelxpi ⊢ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ) → ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝑋 × 𝑌 ) )
14 dfsbcq ⊢ ( 𝑞 = ⟨ 𝑥 , 𝑦 ⟩ → ( [ 𝑞 / 𝑝 ] 𝜓 ↔ [ ⟨ 𝑥 , 𝑦 ⟩ / 𝑝 ] 𝜓 ) )
15 eqeq2 ⊢ ( 𝑞 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝑝 = 𝑞 ↔ 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ ) )
16 14 15 imbi12d ⊢ ( 𝑞 = ⟨ 𝑥 , 𝑦 ⟩ → ( ( [ 𝑞 / 𝑝 ] 𝜓 → 𝑝 = 𝑞 ) ↔ ( [ ⟨ 𝑥 , 𝑦 ⟩ / 𝑝 ] 𝜓 → 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ ) ) )
17 16 adantl ⊢ ( ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ) ∧ 𝑞 = ⟨ 𝑥 , 𝑦 ⟩ ) → ( ( [ 𝑞 / 𝑝 ] 𝜓 → 𝑝 = 𝑞 ) ↔ ( [ ⟨ 𝑥 , 𝑦 ⟩ / 𝑝 ] 𝜓 → 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ ) ) )
18 13 17 rspcdv ⊢ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ) → ( ∀ 𝑞 ∈ ( 𝑋 × 𝑌 ) ( [ 𝑞 / 𝑝 ] 𝜓 → 𝑝 = 𝑞 ) → ( [ ⟨ 𝑥 , 𝑦 ⟩ / 𝑝 ] 𝜓 → 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ ) ) )
19 18 adantr ⊢ ( ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ) ∧ 𝜓 ) → ( ∀ 𝑞 ∈ ( 𝑋 × 𝑌 ) ( [ 𝑞 / 𝑝 ] 𝜓 → 𝑝 = 𝑞 ) → ( [ ⟨ 𝑥 , 𝑦 ⟩ / 𝑝 ] 𝜓 → 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ ) ) )
20 opex ⊢ ⟨ 𝑥 , 𝑦 ⟩ ∈ V
21 20 2 sbcie ⊢ ( [ ⟨ 𝑥 , 𝑦 ⟩ / 𝑝 ] 𝜓 ↔ 𝜃 )
22 pm2.27 ⊢ ( [ ⟨ 𝑥 , 𝑦 ⟩ / 𝑝 ] 𝜓 → ( ( [ ⟨ 𝑥 , 𝑦 ⟩ / 𝑝 ] 𝜓 → 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ ) → 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ ) )
23 21 22 sylbir ⊢ ( 𝜃 → ( ( [ ⟨ 𝑥 , 𝑦 ⟩ / 𝑝 ] 𝜓 → 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ ) → 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ ) )
24 eqcom ⊢ ( ⟨ 𝑥 , 𝑦 ⟩ = 𝑝 ↔ 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ )
25 23 24 syl6ibr ⊢ ( 𝜃 → ( ( [ ⟨ 𝑥 , 𝑦 ⟩ / 𝑝 ] 𝜓 → 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ ) → ⟨ 𝑥 , 𝑦 ⟩ = 𝑝 ) )
26 25 com12 ⊢ ( ( [ ⟨ 𝑥 , 𝑦 ⟩ / 𝑝 ] 𝜓 → 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ ) → ( 𝜃 → ⟨ 𝑥 , 𝑦 ⟩ = 𝑝 ) )
27 eqeq2 ⊢ ( ⟨ 𝑎 , 𝑏 ⟩ = 𝑝 → ( ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ↔ ⟨ 𝑥 , 𝑦 ⟩ = 𝑝 ) )
28 27 eqcoms ⊢ ( 𝑝 = ⟨ 𝑎 , 𝑏 ⟩ → ( ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ↔ ⟨ 𝑥 , 𝑦 ⟩ = 𝑝 ) )
29 28 imbi2d ⊢ ( 𝑝 = ⟨ 𝑎 , 𝑏 ⟩ → ( ( 𝜃 → ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ) ↔ ( 𝜃 → ⟨ 𝑥 , 𝑦 ⟩ = 𝑝 ) ) )
30 26 29 syl5ibrcom ⊢ ( ( [ ⟨ 𝑥 , 𝑦 ⟩ / 𝑝 ] 𝜓 → 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ ) → ( 𝑝 = ⟨ 𝑎 , 𝑏 ⟩ → ( 𝜃 → ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ) ) )
31 30 a1d ⊢ ( ( [ ⟨ 𝑥 , 𝑦 ⟩ / 𝑝 ] 𝜓 → 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ ) → ( ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑌 ) → ( 𝑝 = ⟨ 𝑎 , 𝑏 ⟩ → ( 𝜃 → ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ) ) ) )
32 19 31 syl6 ⊢ ( ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ) ∧ 𝜓 ) → ( ∀ 𝑞 ∈ ( 𝑋 × 𝑌 ) ( [ 𝑞 / 𝑝 ] 𝜓 → 𝑝 = 𝑞 ) → ( ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑌 ) → ( 𝑝 = ⟨ 𝑎 , 𝑏 ⟩ → ( 𝜃 → ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ) ) ) ) )
33 32 expimpd ⊢ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ) → ( ( 𝜓 ∧ ∀ 𝑞 ∈ ( 𝑋 × 𝑌 ) ( [ 𝑞 / 𝑝 ] 𝜓 → 𝑝 = 𝑞 ) ) → ( ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑌 ) → ( 𝑝 = ⟨ 𝑎 , 𝑏 ⟩ → ( 𝜃 → ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ) ) ) ) )
34 33 imp4c ⊢ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ) → ( ( ( ( 𝜓 ∧ ∀ 𝑞 ∈ ( 𝑋 × 𝑌 ) ( [ 𝑞 / 𝑝 ] 𝜓 → 𝑝 = 𝑞 ) ) ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑌 ) ) ∧ 𝑝 = ⟨ 𝑎 , 𝑏 ⟩ ) → ( 𝜃 → ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ) ) )
35 34 impcom ⊢ ( ( ( ( ( 𝜓 ∧ ∀ 𝑞 ∈ ( 𝑋 × 𝑌 ) ( [ 𝑞 / 𝑝 ] 𝜓 → 𝑝 = 𝑞 ) ) ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑌 ) ) ∧ 𝑝 = ⟨ 𝑎 , 𝑏 ⟩ ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ) ) → ( 𝜃 → ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ) )
36 35 ralrimivva ⊢ ( ( ( ( 𝜓 ∧ ∀ 𝑞 ∈ ( 𝑋 × 𝑌 ) ( [ 𝑞 / 𝑝 ] 𝜓 → 𝑝 = 𝑞 ) ) ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑌 ) ) ∧ 𝑝 = ⟨ 𝑎 , 𝑏 ⟩ ) → ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑌 ( 𝜃 → ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ) )
37 12 36 jca ⊢ ( ( ( ( 𝜓 ∧ ∀ 𝑞 ∈ ( 𝑋 × 𝑌 ) ( [ 𝑞 / 𝑝 ] 𝜓 → 𝑝 = 𝑞 ) ) ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑌 ) ) ∧ 𝑝 = ⟨ 𝑎 , 𝑏 ⟩ ) → ( 𝜒 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑌 ( 𝜃 → ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ) ) )
38 37 ex ⊢ ( ( ( 𝜓 ∧ ∀ 𝑞 ∈ ( 𝑋 × 𝑌 ) ( [ 𝑞 / 𝑝 ] 𝜓 → 𝑝 = 𝑞 ) ) ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑌 ) ) → ( 𝑝 = ⟨ 𝑎 , 𝑏 ⟩ → ( 𝜒 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑌 ( 𝜃 → ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ) ) ) )
39 38 reximdvva ⊢ ( ( 𝜓 ∧ ∀ 𝑞 ∈ ( 𝑋 × 𝑌 ) ( [ 𝑞 / 𝑝 ] 𝜓 → 𝑝 = 𝑞 ) ) → ( ∃ 𝑎 ∈ 𝑋 ∃ 𝑏 ∈ 𝑌 𝑝 = ⟨ 𝑎 , 𝑏 ⟩ → ∃ 𝑎 ∈ 𝑋 ∃ 𝑏 ∈ 𝑌 ( 𝜒 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑌 ( 𝜃 → ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ) ) ) )
40 39 com12 ⊢ ( ∃ 𝑎 ∈ 𝑋 ∃ 𝑏 ∈ 𝑌 𝑝 = ⟨ 𝑎 , 𝑏 ⟩ → ( ( 𝜓 ∧ ∀ 𝑞 ∈ ( 𝑋 × 𝑌 ) ( [ 𝑞 / 𝑝 ] 𝜓 → 𝑝 = 𝑞 ) ) → ∃ 𝑎 ∈ 𝑋 ∃ 𝑏 ∈ 𝑌 ( 𝜒 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑌 ( 𝜃 → ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ) ) ) )
41 8 40 sylbi ⊢ ( 𝑝 ∈ ( 𝑋 × 𝑌 ) → ( ( 𝜓 ∧ ∀ 𝑞 ∈ ( 𝑋 × 𝑌 ) ( [ 𝑞 / 𝑝 ] 𝜓 → 𝑝 = 𝑞 ) ) → ∃ 𝑎 ∈ 𝑋 ∃ 𝑏 ∈ 𝑌 ( 𝜒 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑌 ( 𝜃 → ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ) ) ) )
42 41 rexlimiv ⊢ ( ∃ 𝑝 ∈ ( 𝑋 × 𝑌 ) ( 𝜓 ∧ ∀ 𝑞 ∈ ( 𝑋 × 𝑌 ) ( [ 𝑞 / 𝑝 ] 𝜓 → 𝑝 = 𝑞 ) ) → ∃ 𝑎 ∈ 𝑋 ∃ 𝑏 ∈ 𝑌 ( 𝜒 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑌 ( 𝜃 → ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ) ) )
43 opelxpi ⊢ ( ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑌 ) → ⟨ 𝑎 , 𝑏 ⟩ ∈ ( 𝑋 × 𝑌 ) )
44 43 adantr ⊢ ( ( ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑌 ) ∧ ( 𝜒 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑌 ( 𝜃 → ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ) ) ) → ⟨ 𝑎 , 𝑏 ⟩ ∈ ( 𝑋 × 𝑌 ) )
45 simprl ⊢ ( ( ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑌 ) ∧ ( 𝜒 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑌 ( 𝜃 → ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ) ) ) → 𝜒 )
46 nfsbc1v ⊢ Ⅎ 𝑥 [ 𝑐 / 𝑥 ] 𝜃
47 nfv ⊢ Ⅎ 𝑥 ⟨ 𝑐 , 𝑦 ⟩ = ⟨ 𝑎 , 𝑏 ⟩
48 46 47 nfim ⊢ Ⅎ 𝑥 ( [ 𝑐 / 𝑥 ] 𝜃 → ⟨ 𝑐 , 𝑦 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ )
49 nfsbc1v ⊢ Ⅎ 𝑦 [ 𝑑 / 𝑦 ] [ 𝑐 / 𝑥 ] 𝜃
50 nfv ⊢ Ⅎ 𝑦 ⟨ 𝑐 , 𝑑 ⟩ = ⟨ 𝑎 , 𝑏 ⟩
51 49 50 nfim ⊢ Ⅎ 𝑦 ( [ 𝑑 / 𝑦 ] [ 𝑐 / 𝑥 ] 𝜃 → ⟨ 𝑐 , 𝑑 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ )
52 sbceq1a ⊢ ( 𝑥 = 𝑐 → ( 𝜃 ↔ [ 𝑐 / 𝑥 ] 𝜃 ) )
53 opeq1 ⊢ ( 𝑥 = 𝑐 → ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑐 , 𝑦 ⟩ )
54 53 eqeq1d ⊢ ( 𝑥 = 𝑐 → ( ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ↔ ⟨ 𝑐 , 𝑦 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ) )
55 52 54 imbi12d ⊢ ( 𝑥 = 𝑐 → ( ( 𝜃 → ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ) ↔ ( [ 𝑐 / 𝑥 ] 𝜃 → ⟨ 𝑐 , 𝑦 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ) ) )
56 sbceq1a ⊢ ( 𝑦 = 𝑑 → ( [ 𝑐 / 𝑥 ] 𝜃 ↔ [ 𝑑 / 𝑦 ] [ 𝑐 / 𝑥 ] 𝜃 ) )
57 opeq2 ⊢ ( 𝑦 = 𝑑 → ⟨ 𝑐 , 𝑦 ⟩ = ⟨ 𝑐 , 𝑑 ⟩ )
58 57 eqeq1d ⊢ ( 𝑦 = 𝑑 → ( ⟨ 𝑐 , 𝑦 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ↔ ⟨ 𝑐 , 𝑑 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ) )
59 56 58 imbi12d ⊢ ( 𝑦 = 𝑑 → ( ( [ 𝑐 / 𝑥 ] 𝜃 → ⟨ 𝑐 , 𝑦 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ) ↔ ( [ 𝑑 / 𝑦 ] [ 𝑐 / 𝑥 ] 𝜃 → ⟨ 𝑐 , 𝑑 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ) ) )
60 48 51 55 59 rspc2 ⊢ ( ( 𝑐 ∈ 𝑋 ∧ 𝑑 ∈ 𝑌 ) → ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑌 ( 𝜃 → ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ) → ( [ 𝑑 / 𝑦 ] [ 𝑐 / 𝑥 ] 𝜃 → ⟨ 𝑐 , 𝑑 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ) ) )
61 60 ad2antlr ⊢ ( ( ( ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑌 ) ∧ ( 𝑐 ∈ 𝑋 ∧ 𝑑 ∈ 𝑌 ) ) ∧ 𝜒 ) → ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑌 ( 𝜃 → ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ) → ( [ 𝑑 / 𝑦 ] [ 𝑐 / 𝑥 ] 𝜃 → ⟨ 𝑐 , 𝑑 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ) ) )
62 2 sbcop ⊢ ( [ 𝑑 / 𝑦 ] [ 𝑐 / 𝑥 ] 𝜃 ↔ [ ⟨ 𝑐 , 𝑑 ⟩ / 𝑝 ] 𝜓 )
63 pm2.27 ⊢ ( [ 𝑑 / 𝑦 ] [ 𝑐 / 𝑥 ] 𝜃 → ( ( [ 𝑑 / 𝑦 ] [ 𝑐 / 𝑥 ] 𝜃 → ⟨ 𝑐 , 𝑑 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ) → ⟨ 𝑐 , 𝑑 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ) )
64 62 63 sylbir ⊢ ( [ ⟨ 𝑐 , 𝑑 ⟩ / 𝑝 ] 𝜓 → ( ( [ 𝑑 / 𝑦 ] [ 𝑐 / 𝑥 ] 𝜃 → ⟨ 𝑐 , 𝑑 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ) → ⟨ 𝑐 , 𝑑 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ) )
65 eqcom ⊢ ( ⟨ 𝑎 , 𝑏 ⟩ = ⟨ 𝑐 , 𝑑 ⟩ ↔ ⟨ 𝑐 , 𝑑 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ )
66 64 65 syl6ibr ⊢ ( [ ⟨ 𝑐 , 𝑑 ⟩ / 𝑝 ] 𝜓 → ( ( [ 𝑑 / 𝑦 ] [ 𝑐 / 𝑥 ] 𝜃 → ⟨ 𝑐 , 𝑑 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ) → ⟨ 𝑎 , 𝑏 ⟩ = ⟨ 𝑐 , 𝑑 ⟩ ) )
67 66 com12 ⊢ ( ( [ 𝑑 / 𝑦 ] [ 𝑐 / 𝑥 ] 𝜃 → ⟨ 𝑐 , 𝑑 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ) → ( [ ⟨ 𝑐 , 𝑑 ⟩ / 𝑝 ] 𝜓 → ⟨ 𝑎 , 𝑏 ⟩ = ⟨ 𝑐 , 𝑑 ⟩ ) )
68 61 67 syl6 ⊢ ( ( ( ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑌 ) ∧ ( 𝑐 ∈ 𝑋 ∧ 𝑑 ∈ 𝑌 ) ) ∧ 𝜒 ) → ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑌 ( 𝜃 → ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ) → ( [ ⟨ 𝑐 , 𝑑 ⟩ / 𝑝 ] 𝜓 → ⟨ 𝑎 , 𝑏 ⟩ = ⟨ 𝑐 , 𝑑 ⟩ ) ) )
69 68 expimpd ⊢ ( ( ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑌 ) ∧ ( 𝑐 ∈ 𝑋 ∧ 𝑑 ∈ 𝑌 ) ) → ( ( 𝜒 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑌 ( 𝜃 → ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ) ) → ( [ ⟨ 𝑐 , 𝑑 ⟩ / 𝑝 ] 𝜓 → ⟨ 𝑎 , 𝑏 ⟩ = ⟨ 𝑐 , 𝑑 ⟩ ) ) )
70 69 expcom ⊢ ( ( 𝑐 ∈ 𝑋 ∧ 𝑑 ∈ 𝑌 ) → ( ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑌 ) → ( ( 𝜒 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑌 ( 𝜃 → ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ) ) → ( [ ⟨ 𝑐 , 𝑑 ⟩ / 𝑝 ] 𝜓 → ⟨ 𝑎 , 𝑏 ⟩ = ⟨ 𝑐 , 𝑑 ⟩ ) ) ) )
71 70 impd ⊢ ( ( 𝑐 ∈ 𝑋 ∧ 𝑑 ∈ 𝑌 ) → ( ( ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑌 ) ∧ ( 𝜒 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑌 ( 𝜃 → ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ) ) ) → ( [ ⟨ 𝑐 , 𝑑 ⟩ / 𝑝 ] 𝜓 → ⟨ 𝑎 , 𝑏 ⟩ = ⟨ 𝑐 , 𝑑 ⟩ ) ) )
72 71 impcom ⊢ ( ( ( ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑌 ) ∧ ( 𝜒 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑌 ( 𝜃 → ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ) ) ) ∧ ( 𝑐 ∈ 𝑋 ∧ 𝑑 ∈ 𝑌 ) ) → ( [ ⟨ 𝑐 , 𝑑 ⟩ / 𝑝 ] 𝜓 → ⟨ 𝑎 , 𝑏 ⟩ = ⟨ 𝑐 , 𝑑 ⟩ ) )
73 dfsbcq ⊢ ( 𝑞 = ⟨ 𝑐 , 𝑑 ⟩ → ( [ 𝑞 / 𝑝 ] 𝜓 ↔ [ ⟨ 𝑐 , 𝑑 ⟩ / 𝑝 ] 𝜓 ) )
74 eqeq2 ⊢ ( 𝑞 = ⟨ 𝑐 , 𝑑 ⟩ → ( ⟨ 𝑎 , 𝑏 ⟩ = 𝑞 ↔ ⟨ 𝑎 , 𝑏 ⟩ = ⟨ 𝑐 , 𝑑 ⟩ ) )
75 73 74 imbi12d ⊢ ( 𝑞 = ⟨ 𝑐 , 𝑑 ⟩ → ( ( [ 𝑞 / 𝑝 ] 𝜓 → ⟨ 𝑎 , 𝑏 ⟩ = 𝑞 ) ↔ ( [ ⟨ 𝑐 , 𝑑 ⟩ / 𝑝 ] 𝜓 → ⟨ 𝑎 , 𝑏 ⟩ = ⟨ 𝑐 , 𝑑 ⟩ ) ) )
76 72 75 syl5ibrcom ⊢ ( ( ( ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑌 ) ∧ ( 𝜒 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑌 ( 𝜃 → ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ) ) ) ∧ ( 𝑐 ∈ 𝑋 ∧ 𝑑 ∈ 𝑌 ) ) → ( 𝑞 = ⟨ 𝑐 , 𝑑 ⟩ → ( [ 𝑞 / 𝑝 ] 𝜓 → ⟨ 𝑎 , 𝑏 ⟩ = 𝑞 ) ) )
77 76 rexlimdvva ⊢ ( ( ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑌 ) ∧ ( 𝜒 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑌 ( 𝜃 → ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ) ) ) → ( ∃ 𝑐 ∈ 𝑋 ∃ 𝑑 ∈ 𝑌 𝑞 = ⟨ 𝑐 , 𝑑 ⟩ → ( [ 𝑞 / 𝑝 ] 𝜓 → ⟨ 𝑎 , 𝑏 ⟩ = 𝑞 ) ) )
78 elxp2 ⊢ ( 𝑞 ∈ ( 𝑋 × 𝑌 ) ↔ ∃ 𝑐 ∈ 𝑋 ∃ 𝑑 ∈ 𝑌 𝑞 = ⟨ 𝑐 , 𝑑 ⟩ )
79 78 biimpi ⊢ ( 𝑞 ∈ ( 𝑋 × 𝑌 ) → ∃ 𝑐 ∈ 𝑋 ∃ 𝑑 ∈ 𝑌 𝑞 = ⟨ 𝑐 , 𝑑 ⟩ )
80 77 79 impel ⊢ ( ( ( ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑌 ) ∧ ( 𝜒 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑌 ( 𝜃 → ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ) ) ) ∧ 𝑞 ∈ ( 𝑋 × 𝑌 ) ) → ( [ 𝑞 / 𝑝 ] 𝜓 → ⟨ 𝑎 , 𝑏 ⟩ = 𝑞 ) )
81 80 ralrimiva ⊢ ( ( ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑌 ) ∧ ( 𝜒 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑌 ( 𝜃 → ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ) ) ) → ∀ 𝑞 ∈ ( 𝑋 × 𝑌 ) ( [ 𝑞 / 𝑝 ] 𝜓 → ⟨ 𝑎 , 𝑏 ⟩ = 𝑞 ) )
82 nfv ⊢ Ⅎ 𝑝 𝜒
83 nfcv ⊢ Ⅎ 𝑝 ( 𝑋 × 𝑌 )
84 nfv ⊢ Ⅎ 𝑝 ⟨ 𝑎 , 𝑏 ⟩ = 𝑞
85 3 84 nfim ⊢ Ⅎ 𝑝 ( [ 𝑞 / 𝑝 ] 𝜓 → ⟨ 𝑎 , 𝑏 ⟩ = 𝑞 )
86 83 85 nfralw ⊢ Ⅎ 𝑝 ∀ 𝑞 ∈ ( 𝑋 × 𝑌 ) ( [ 𝑞 / 𝑝 ] 𝜓 → ⟨ 𝑎 , 𝑏 ⟩ = 𝑞 )
87 82 86 nfan ⊢ Ⅎ 𝑝 ( 𝜒 ∧ ∀ 𝑞 ∈ ( 𝑋 × 𝑌 ) ( [ 𝑞 / 𝑝 ] 𝜓 → ⟨ 𝑎 , 𝑏 ⟩ = 𝑞 ) )
88 eqeq1 ⊢ ( 𝑝 = ⟨ 𝑎 , 𝑏 ⟩ → ( 𝑝 = 𝑞 ↔ ⟨ 𝑎 , 𝑏 ⟩ = 𝑞 ) )
89 88 imbi2d ⊢ ( 𝑝 = ⟨ 𝑎 , 𝑏 ⟩ → ( ( [ 𝑞 / 𝑝 ] 𝜓 → 𝑝 = 𝑞 ) ↔ ( [ 𝑞 / 𝑝 ] 𝜓 → ⟨ 𝑎 , 𝑏 ⟩ = 𝑞 ) ) )
90 89 ralbidv ⊢ ( 𝑝 = ⟨ 𝑎 , 𝑏 ⟩ → ( ∀ 𝑞 ∈ ( 𝑋 × 𝑌 ) ( [ 𝑞 / 𝑝 ] 𝜓 → 𝑝 = 𝑞 ) ↔ ∀ 𝑞 ∈ ( 𝑋 × 𝑌 ) ( [ 𝑞 / 𝑝 ] 𝜓 → ⟨ 𝑎 , 𝑏 ⟩ = 𝑞 ) ) )
91 1 90 anbi12d ⊢ ( 𝑝 = ⟨ 𝑎 , 𝑏 ⟩ → ( ( 𝜓 ∧ ∀ 𝑞 ∈ ( 𝑋 × 𝑌 ) ( [ 𝑞 / 𝑝 ] 𝜓 → 𝑝 = 𝑞 ) ) ↔ ( 𝜒 ∧ ∀ 𝑞 ∈ ( 𝑋 × 𝑌 ) ( [ 𝑞 / 𝑝 ] 𝜓 → ⟨ 𝑎 , 𝑏 ⟩ = 𝑞 ) ) ) )
92 87 91 rspce ⊢ ( ( ⟨ 𝑎 , 𝑏 ⟩ ∈ ( 𝑋 × 𝑌 ) ∧ ( 𝜒 ∧ ∀ 𝑞 ∈ ( 𝑋 × 𝑌 ) ( [ 𝑞 / 𝑝 ] 𝜓 → ⟨ 𝑎 , 𝑏 ⟩ = 𝑞 ) ) ) → ∃ 𝑝 ∈ ( 𝑋 × 𝑌 ) ( 𝜓 ∧ ∀ 𝑞 ∈ ( 𝑋 × 𝑌 ) ( [ 𝑞 / 𝑝 ] 𝜓 → 𝑝 = 𝑞 ) ) )
93 44 45 81 92 syl12anc ⊢ ( ( ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑌 ) ∧ ( 𝜒 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑌 ( 𝜃 → ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ) ) ) → ∃ 𝑝 ∈ ( 𝑋 × 𝑌 ) ( 𝜓 ∧ ∀ 𝑞 ∈ ( 𝑋 × 𝑌 ) ( [ 𝑞 / 𝑝 ] 𝜓 → 𝑝 = 𝑞 ) ) )
94 93 ex ⊢ ( ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑌 ) → ( ( 𝜒 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑌 ( 𝜃 → ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ) ) → ∃ 𝑝 ∈ ( 𝑋 × 𝑌 ) ( 𝜓 ∧ ∀ 𝑞 ∈ ( 𝑋 × 𝑌 ) ( [ 𝑞 / 𝑝 ] 𝜓 → 𝑝 = 𝑞 ) ) ) )
95 94 rexlimivv ⊢ ( ∃ 𝑎 ∈ 𝑋 ∃ 𝑏 ∈ 𝑌 ( 𝜒 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑌 ( 𝜃 → ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ) ) → ∃ 𝑝 ∈ ( 𝑋 × 𝑌 ) ( 𝜓 ∧ ∀ 𝑞 ∈ ( 𝑋 × 𝑌 ) ( [ 𝑞 / 𝑝 ] 𝜓 → 𝑝 = 𝑞 ) ) )
96 42 95 impbii ⊢ ( ∃ 𝑝 ∈ ( 𝑋 × 𝑌 ) ( 𝜓 ∧ ∀ 𝑞 ∈ ( 𝑋 × 𝑌 ) ( [ 𝑞 / 𝑝 ] 𝜓 → 𝑝 = 𝑞 ) ) ↔ ∃ 𝑎 ∈ 𝑋 ∃ 𝑏 ∈ 𝑌 ( 𝜒 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑌 ( 𝜃 → ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ) ) )
97 7 96 bitri ⊢ ( ∃! 𝑝 ∈ ( 𝑋 × 𝑌 ) 𝜓 ↔ ∃ 𝑎 ∈ 𝑋 ∃ 𝑏 ∈ 𝑌 ( 𝜒 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑌 ( 𝜃 → ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ) ) )