Metamath Proof Explorer

Theorem reuopreuprim

Description: There is a unique unordered pair with ordered elements fulfilling a wff if there is a unique ordered pair fulfilling the wff. (Contributed by AV, 28-Jul-2023)

Ref Expression
Assertion reuopreuprim ( 𝑋 ∈ 𝑉 → ( ∃! 𝑝 ∈ ( 𝑋 × 𝑋 ) ∃ 𝑎 ∃ 𝑏 ( 𝑝 = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜑 ) → ∃! 𝑝 ∈ ( Pairs ‘ 𝑋 ) ∃ 𝑎 ∃ 𝑏 ( 𝑝 = { 𝑎 , 𝑏 } ∧ 𝜑 ) ) )

Proof

Step Hyp Ref Expression
1 eqeq1 ⊢ ( 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝑝 = ⟨ 𝑎 , 𝑏 ⟩ ↔ ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ) )
2 1 anbi1d ⊢ ( 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ → ( ( 𝑝 = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜑 ) ↔ ( ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜑 ) ) )
3 2 2exbidv ⊢ ( 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ → ( ∃ 𝑎 ∃ 𝑏 ( 𝑝 = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜑 ) ↔ ∃ 𝑎 ∃ 𝑏 ( ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜑 ) ) )
4 eqeq1 ⊢ ( 𝑝 = ⟨ 𝑖 , 𝑗 ⟩ → ( 𝑝 = ⟨ 𝑎 , 𝑏 ⟩ ↔ ⟨ 𝑖 , 𝑗 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ) )
5 4 anbi1d ⊢ ( 𝑝 = ⟨ 𝑖 , 𝑗 ⟩ → ( ( 𝑝 = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜑 ) ↔ ( ⟨ 𝑖 , 𝑗 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜑 ) ) )
6 5 2exbidv ⊢ ( 𝑝 = ⟨ 𝑖 , 𝑗 ⟩ → ( ∃ 𝑎 ∃ 𝑏 ( 𝑝 = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜑 ) ↔ ∃ 𝑎 ∃ 𝑏 ( ⟨ 𝑖 , 𝑗 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜑 ) ) )
7 3 6 reuop ⊢ ( ∃! 𝑝 ∈ ( 𝑋 × 𝑋 ) ∃ 𝑎 ∃ 𝑏 ( 𝑝 = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜑 ) ↔ ∃ 𝑥 ∈ 𝑋 ∃ 𝑦 ∈ 𝑋 ( ∃ 𝑎 ∃ 𝑏 ( ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜑 ) ∧ ∀ 𝑖 ∈ 𝑋 ∀ 𝑗 ∈ 𝑋 ( ∃ 𝑎 ∃ 𝑏 ( ⟨ 𝑖 , 𝑗 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜑 ) → ⟨ 𝑖 , 𝑗 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ) ) )
8 simpll ⊢ ( ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ∧ ( ∃ 𝑎 ∃ 𝑏 ( ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜑 ) ∧ ∀ 𝑖 ∈ 𝑋 ∀ 𝑗 ∈ 𝑋 ( ∃ 𝑎 ∃ 𝑏 ( ⟨ 𝑖 , 𝑗 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜑 ) → ⟨ 𝑖 , 𝑗 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ) ) ) → 𝑥 ∈ 𝑋 )
9 simplr ⊢ ( ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ∧ ( ∃ 𝑎 ∃ 𝑏 ( ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜑 ) ∧ ∀ 𝑖 ∈ 𝑋 ∀ 𝑗 ∈ 𝑋 ( ∃ 𝑎 ∃ 𝑏 ( ⟨ 𝑖 , 𝑗 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜑 ) → ⟨ 𝑖 , 𝑗 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ) ) ) → 𝑦 ∈ 𝑋 )
10 oppr ⊢ ( ( 𝑥 ∈ V ∧ 𝑦 ∈ V ) → ( ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ → { 𝑥 , 𝑦 } = { 𝑎 , 𝑏 } ) )
11 10 el2v ⊢ ( ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ → { 𝑥 , 𝑦 } = { 𝑎 , 𝑏 } )
12 11 anim1i ⊢ ( ( ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜑 ) → ( { 𝑥 , 𝑦 } = { 𝑎 , 𝑏 } ∧ 𝜑 ) )
13 12 2eximi ⊢ ( ∃ 𝑎 ∃ 𝑏 ( ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜑 ) → ∃ 𝑎 ∃ 𝑏 ( { 𝑥 , 𝑦 } = { 𝑎 , 𝑏 } ∧ 𝜑 ) )
14 13 adantr ⊢ ( ( ∃ 𝑎 ∃ 𝑏 ( ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜑 ) ∧ ∀ 𝑖 ∈ 𝑋 ∀ 𝑗 ∈ 𝑋 ( ∃ 𝑎 ∃ 𝑏 ( ⟨ 𝑖 , 𝑗 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜑 ) → ⟨ 𝑖 , 𝑗 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ) ) → ∃ 𝑎 ∃ 𝑏 ( { 𝑥 , 𝑦 } = { 𝑎 , 𝑏 } ∧ 𝜑 ) )
15 14 adantl ⊢ ( ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ∧ ( ∃ 𝑎 ∃ 𝑏 ( ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜑 ) ∧ ∀ 𝑖 ∈ 𝑋 ∀ 𝑗 ∈ 𝑋 ( ∃ 𝑎 ∃ 𝑏 ( ⟨ 𝑖 , 𝑗 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜑 ) → ⟨ 𝑖 , 𝑗 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ) ) ) → ∃ 𝑎 ∃ 𝑏 ( { 𝑥 , 𝑦 } = { 𝑎 , 𝑏 } ∧ 𝜑 ) )
16 nfv ⊢ Ⅎ 𝑎 ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 )
17 nfe1 ⊢ Ⅎ 𝑎 ∃ 𝑎 ∃ 𝑏 ( ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜑 )
18 nfcv ⊢ Ⅎ 𝑎 𝑋
19 nfe1 ⊢ Ⅎ 𝑎 ∃ 𝑎 ∃ 𝑏 ( ⟨ 𝑖 , 𝑗 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜑 )
20 nfv ⊢ Ⅎ 𝑎 ⟨ 𝑖 , 𝑗 ⟩ = ⟨ 𝑥 , 𝑦 ⟩
21 19 20 nfim ⊢ Ⅎ 𝑎 ( ∃ 𝑎 ∃ 𝑏 ( ⟨ 𝑖 , 𝑗 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜑 ) → ⟨ 𝑖 , 𝑗 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ )
22 18 21 nfralw ⊢ Ⅎ 𝑎 ∀ 𝑗 ∈ 𝑋 ( ∃ 𝑎 ∃ 𝑏 ( ⟨ 𝑖 , 𝑗 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜑 ) → ⟨ 𝑖 , 𝑗 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ )
23 18 22 nfralw ⊢ Ⅎ 𝑎 ∀ 𝑖 ∈ 𝑋 ∀ 𝑗 ∈ 𝑋 ( ∃ 𝑎 ∃ 𝑏 ( ⟨ 𝑖 , 𝑗 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜑 ) → ⟨ 𝑖 , 𝑗 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ )
24 17 23 nfan ⊢ Ⅎ 𝑎 ( ∃ 𝑎 ∃ 𝑏 ( ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜑 ) ∧ ∀ 𝑖 ∈ 𝑋 ∀ 𝑗 ∈ 𝑋 ( ∃ 𝑎 ∃ 𝑏 ( ⟨ 𝑖 , 𝑗 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜑 ) → ⟨ 𝑖 , 𝑗 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ) )
25 16 24 nfan ⊢ Ⅎ 𝑎 ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ∧ ( ∃ 𝑎 ∃ 𝑏 ( ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜑 ) ∧ ∀ 𝑖 ∈ 𝑋 ∀ 𝑗 ∈ 𝑋 ( ∃ 𝑎 ∃ 𝑏 ( ⟨ 𝑖 , 𝑗 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜑 ) → ⟨ 𝑖 , 𝑗 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ) ) )
26 nfv ⊢ Ⅎ 𝑎 ( 𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑋 )
27 25 26 nfan ⊢ Ⅎ 𝑎 ( ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ∧ ( ∃ 𝑎 ∃ 𝑏 ( ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜑 ) ∧ ∀ 𝑖 ∈ 𝑋 ∀ 𝑗 ∈ 𝑋 ( ∃ 𝑎 ∃ 𝑏 ( ⟨ 𝑖 , 𝑗 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜑 ) → ⟨ 𝑖 , 𝑗 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ) ) ) ∧ ( 𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑋 ) )
28 nfv ⊢ Ⅎ 𝑎 { 𝑚 , 𝑛 } = { 𝑥 , 𝑦 }
29 nfv ⊢ Ⅎ 𝑏 ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 )
30 nfe1 ⊢ Ⅎ 𝑏 ∃ 𝑏 ( ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜑 )
31 30 nfex ⊢ Ⅎ 𝑏 ∃ 𝑎 ∃ 𝑏 ( ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜑 )
32 nfcv ⊢ Ⅎ 𝑏 𝑋
33 nfe1 ⊢ Ⅎ 𝑏 ∃ 𝑏 ( ⟨ 𝑖 , 𝑗 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜑 )
34 33 nfex ⊢ Ⅎ 𝑏 ∃ 𝑎 ∃ 𝑏 ( ⟨ 𝑖 , 𝑗 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜑 )
35 nfv ⊢ Ⅎ 𝑏 ⟨ 𝑖 , 𝑗 ⟩ = ⟨ 𝑥 , 𝑦 ⟩
36 34 35 nfim ⊢ Ⅎ 𝑏 ( ∃ 𝑎 ∃ 𝑏 ( ⟨ 𝑖 , 𝑗 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜑 ) → ⟨ 𝑖 , 𝑗 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ )
37 32 36 nfralw ⊢ Ⅎ 𝑏 ∀ 𝑗 ∈ 𝑋 ( ∃ 𝑎 ∃ 𝑏 ( ⟨ 𝑖 , 𝑗 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜑 ) → ⟨ 𝑖 , 𝑗 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ )
38 32 37 nfralw ⊢ Ⅎ 𝑏 ∀ 𝑖 ∈ 𝑋 ∀ 𝑗 ∈ 𝑋 ( ∃ 𝑎 ∃ 𝑏 ( ⟨ 𝑖 , 𝑗 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜑 ) → ⟨ 𝑖 , 𝑗 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ )
39 31 38 nfan ⊢ Ⅎ 𝑏 ( ∃ 𝑎 ∃ 𝑏 ( ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜑 ) ∧ ∀ 𝑖 ∈ 𝑋 ∀ 𝑗 ∈ 𝑋 ( ∃ 𝑎 ∃ 𝑏 ( ⟨ 𝑖 , 𝑗 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜑 ) → ⟨ 𝑖 , 𝑗 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ) )
40 29 39 nfan ⊢ Ⅎ 𝑏 ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ∧ ( ∃ 𝑎 ∃ 𝑏 ( ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜑 ) ∧ ∀ 𝑖 ∈ 𝑋 ∀ 𝑗 ∈ 𝑋 ( ∃ 𝑎 ∃ 𝑏 ( ⟨ 𝑖 , 𝑗 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜑 ) → ⟨ 𝑖 , 𝑗 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ) ) )
41 nfv ⊢ Ⅎ 𝑏 ( 𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑋 )
42 40 41 nfan ⊢ Ⅎ 𝑏 ( ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ∧ ( ∃ 𝑎 ∃ 𝑏 ( ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜑 ) ∧ ∀ 𝑖 ∈ 𝑋 ∀ 𝑗 ∈ 𝑋 ( ∃ 𝑎 ∃ 𝑏 ( ⟨ 𝑖 , 𝑗 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜑 ) → ⟨ 𝑖 , 𝑗 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ) ) ) ∧ ( 𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑋 ) )
43 nfv ⊢ Ⅎ 𝑏 { 𝑚 , 𝑛 } = { 𝑥 , 𝑦 }
44 vex ⊢ 𝑚 ∈ V
45 vex ⊢ 𝑛 ∈ V
46 vex ⊢ 𝑎 ∈ V
47 vex ⊢ 𝑏 ∈ V
48 44 45 46 47 preq12b ⊢ ( { 𝑚 , 𝑛 } = { 𝑎 , 𝑏 } ↔ ( ( 𝑚 = 𝑎 ∧ 𝑛 = 𝑏 ) ∨ ( 𝑚 = 𝑏 ∧ 𝑛 = 𝑎 ) ) )
49 opeq1 ⊢ ( 𝑖 = 𝑚 → ⟨ 𝑖 , 𝑗 ⟩ = ⟨ 𝑚 , 𝑗 ⟩ )
50 49 eqeq1d ⊢ ( 𝑖 = 𝑚 → ( ⟨ 𝑖 , 𝑗 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ↔ ⟨ 𝑚 , 𝑗 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ) )
51 50 anbi1d ⊢ ( 𝑖 = 𝑚 → ( ( ⟨ 𝑖 , 𝑗 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜑 ) ↔ ( ⟨ 𝑚 , 𝑗 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜑 ) ) )
52 51 2exbidv ⊢ ( 𝑖 = 𝑚 → ( ∃ 𝑎 ∃ 𝑏 ( ⟨ 𝑖 , 𝑗 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜑 ) ↔ ∃ 𝑎 ∃ 𝑏 ( ⟨ 𝑚 , 𝑗 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜑 ) ) )
53 49 eqeq1d ⊢ ( 𝑖 = 𝑚 → ( ⟨ 𝑖 , 𝑗 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ↔ ⟨ 𝑚 , 𝑗 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ) )
54 52 53 imbi12d ⊢ ( 𝑖 = 𝑚 → ( ( ∃ 𝑎 ∃ 𝑏 ( ⟨ 𝑖 , 𝑗 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜑 ) → ⟨ 𝑖 , 𝑗 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ) ↔ ( ∃ 𝑎 ∃ 𝑏 ( ⟨ 𝑚 , 𝑗 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜑 ) → ⟨ 𝑚 , 𝑗 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ) ) )
55 opeq2 ⊢ ( 𝑗 = 𝑛 → ⟨ 𝑚 , 𝑗 ⟩ = ⟨ 𝑚 , 𝑛 ⟩ )
56 55 eqeq1d ⊢ ( 𝑗 = 𝑛 → ( ⟨ 𝑚 , 𝑗 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ↔ ⟨ 𝑚 , 𝑛 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ) )
57 56 anbi1d ⊢ ( 𝑗 = 𝑛 → ( ( ⟨ 𝑚 , 𝑗 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜑 ) ↔ ( ⟨ 𝑚 , 𝑛 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜑 ) ) )
58 57 2exbidv ⊢ ( 𝑗 = 𝑛 → ( ∃ 𝑎 ∃ 𝑏 ( ⟨ 𝑚 , 𝑗 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜑 ) ↔ ∃ 𝑎 ∃ 𝑏 ( ⟨ 𝑚 , 𝑛 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜑 ) ) )
59 55 eqeq1d ⊢ ( 𝑗 = 𝑛 → ( ⟨ 𝑚 , 𝑗 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ↔ ⟨ 𝑚 , 𝑛 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ) )
60 58 59 imbi12d ⊢ ( 𝑗 = 𝑛 → ( ( ∃ 𝑎 ∃ 𝑏 ( ⟨ 𝑚 , 𝑗 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜑 ) → ⟨ 𝑚 , 𝑗 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ) ↔ ( ∃ 𝑎 ∃ 𝑏 ( ⟨ 𝑚 , 𝑛 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜑 ) → ⟨ 𝑚 , 𝑛 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ) ) )
61 54 60 rspc2v ⊢ ( ( 𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑋 ) → ( ∀ 𝑖 ∈ 𝑋 ∀ 𝑗 ∈ 𝑋 ( ∃ 𝑎 ∃ 𝑏 ( ⟨ 𝑖 , 𝑗 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜑 ) → ⟨ 𝑖 , 𝑗 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ) → ( ∃ 𝑎 ∃ 𝑏 ( ⟨ 𝑚 , 𝑛 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜑 ) → ⟨ 𝑚 , 𝑛 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ) ) )
62 pm3.22 ⊢ ( ( ( 𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑋 ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑋 ) ) )
63 62 3adant2 ⊢ ( ( ( 𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑋 ) ∧ ( 𝑚 = 𝑎 ∧ 𝑛 = 𝑏 ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑋 ) ) )
64 63 adantr ⊢ ( ( ( ( 𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑋 ) ∧ ( 𝑚 = 𝑎 ∧ 𝑛 = 𝑏 ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ 𝜑 ) → ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑋 ) ) )
65 eqidd ⊢ ( ( ( ( 𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑋 ) ∧ ( 𝑚 = 𝑎 ∧ 𝑛 = 𝑏 ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ 𝜑 ) → ⟨ 𝑚 , 𝑛 ⟩ = ⟨ 𝑚 , 𝑛 ⟩ )
66 sbceq1a ⊢ ( 𝑎 = 𝑚 → ( 𝜑 ↔ [ 𝑚 / 𝑎 ] 𝜑 ) )
67 66 equcoms ⊢ ( 𝑚 = 𝑎 → ( 𝜑 ↔ [ 𝑚 / 𝑎 ] 𝜑 ) )
68 sbceq1a ⊢ ( 𝑏 = 𝑛 → ( [ 𝑚 / 𝑎 ] 𝜑 ↔ [ 𝑛 / 𝑏 ] [ 𝑚 / 𝑎 ] 𝜑 ) )
69 68 equcoms ⊢ ( 𝑛 = 𝑏 → ( [ 𝑚 / 𝑎 ] 𝜑 ↔ [ 𝑛 / 𝑏 ] [ 𝑚 / 𝑎 ] 𝜑 ) )
70 67 69 sylan9bb ⊢ ( ( 𝑚 = 𝑎 ∧ 𝑛 = 𝑏 ) → ( 𝜑 ↔ [ 𝑛 / 𝑏 ] [ 𝑚 / 𝑎 ] 𝜑 ) )
71 70 3ad2ant2 ⊢ ( ( ( 𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑋 ) ∧ ( 𝑚 = 𝑎 ∧ 𝑛 = 𝑏 ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( 𝜑 ↔ [ 𝑛 / 𝑏 ] [ 𝑚 / 𝑎 ] 𝜑 ) )
72 71 biimpa ⊢ ( ( ( ( 𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑋 ) ∧ ( 𝑚 = 𝑎 ∧ 𝑛 = 𝑏 ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ 𝜑 ) → [ 𝑛 / 𝑏 ] [ 𝑚 / 𝑎 ] 𝜑 )
73 64 65 72 jca32 ⊢ ( ( ( ( 𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑋 ) ∧ ( 𝑚 = 𝑎 ∧ 𝑛 = 𝑏 ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ 𝜑 ) → ( ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑋 ) ) ∧ ( ⟨ 𝑚 , 𝑛 ⟩ = ⟨ 𝑚 , 𝑛 ⟩ ∧ [ 𝑛 / 𝑏 ] [ 𝑚 / 𝑎 ] 𝜑 ) ) )
74 nfv ⊢ Ⅎ 𝑎 ⟨ 𝑚 , 𝑛 ⟩ = ⟨ 𝑚 , 𝑛 ⟩
75 nfcv ⊢ Ⅎ 𝑎 𝑛
76 nfsbc1v ⊢ Ⅎ 𝑎 [ 𝑚 / 𝑎 ] 𝜑
77 75 76 nfsbcw ⊢ Ⅎ 𝑎 [ 𝑛 / 𝑏 ] [ 𝑚 / 𝑎 ] 𝜑
78 74 77 nfan ⊢ Ⅎ 𝑎 ( ⟨ 𝑚 , 𝑛 ⟩ = ⟨ 𝑚 , 𝑛 ⟩ ∧ [ 𝑛 / 𝑏 ] [ 𝑚 / 𝑎 ] 𝜑 )
79 nfv ⊢ Ⅎ 𝑏 ⟨ 𝑚 , 𝑛 ⟩ = ⟨ 𝑚 , 𝑛 ⟩
80 nfsbc1v ⊢ Ⅎ 𝑏 [ 𝑛 / 𝑏 ] [ 𝑚 / 𝑎 ] 𝜑
81 79 80 nfan ⊢ Ⅎ 𝑏 ( ⟨ 𝑚 , 𝑛 ⟩ = ⟨ 𝑚 , 𝑛 ⟩ ∧ [ 𝑛 / 𝑏 ] [ 𝑚 / 𝑎 ] 𝜑 )
82 opeq12 ⊢ ( ( 𝑎 = 𝑚 ∧ 𝑏 = 𝑛 ) → ⟨ 𝑎 , 𝑏 ⟩ = ⟨ 𝑚 , 𝑛 ⟩ )
83 82 eqeq2d ⊢ ( ( 𝑎 = 𝑚 ∧ 𝑏 = 𝑛 ) → ( ⟨ 𝑚 , 𝑛 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ↔ ⟨ 𝑚 , 𝑛 ⟩ = ⟨ 𝑚 , 𝑛 ⟩ ) )
84 66 68 sylan9bb ⊢ ( ( 𝑎 = 𝑚 ∧ 𝑏 = 𝑛 ) → ( 𝜑 ↔ [ 𝑛 / 𝑏 ] [ 𝑚 / 𝑎 ] 𝜑 ) )
85 83 84 anbi12d ⊢ ( ( 𝑎 = 𝑚 ∧ 𝑏 = 𝑛 ) → ( ( ⟨ 𝑚 , 𝑛 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜑 ) ↔ ( ⟨ 𝑚 , 𝑛 ⟩ = ⟨ 𝑚 , 𝑛 ⟩ ∧ [ 𝑛 / 𝑏 ] [ 𝑚 / 𝑎 ] 𝜑 ) ) )
86 85 adantl ⊢ ( ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝑎 = 𝑚 ∧ 𝑏 = 𝑛 ) ) → ( ( ⟨ 𝑚 , 𝑛 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜑 ) ↔ ( ⟨ 𝑚 , 𝑛 ⟩ = ⟨ 𝑚 , 𝑛 ⟩ ∧ [ 𝑛 / 𝑏 ] [ 𝑚 / 𝑎 ] 𝜑 ) ) )
87 78 81 86 spc2ed ⊢ ( ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑋 ) ) → ( ( ⟨ 𝑚 , 𝑛 ⟩ = ⟨ 𝑚 , 𝑛 ⟩ ∧ [ 𝑛 / 𝑏 ] [ 𝑚 / 𝑎 ] 𝜑 ) → ∃ 𝑎 ∃ 𝑏 ( ⟨ 𝑚 , 𝑛 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜑 ) ) )
88 87 imp ⊢ ( ( ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑋 ) ) ∧ ( ⟨ 𝑚 , 𝑛 ⟩ = ⟨ 𝑚 , 𝑛 ⟩ ∧ [ 𝑛 / 𝑏 ] [ 𝑚 / 𝑎 ] 𝜑 ) ) → ∃ 𝑎 ∃ 𝑏 ( ⟨ 𝑚 , 𝑛 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜑 ) )
89 pm2.27 ⊢ ( ∃ 𝑎 ∃ 𝑏 ( ⟨ 𝑚 , 𝑛 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜑 ) → ( ( ∃ 𝑎 ∃ 𝑏 ( ⟨ 𝑚 , 𝑛 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜑 ) → ⟨ 𝑚 , 𝑛 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ) → ⟨ 𝑚 , 𝑛 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ) )
90 73 88 89 3syl ⊢ ( ( ( ( 𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑋 ) ∧ ( 𝑚 = 𝑎 ∧ 𝑛 = 𝑏 ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ 𝜑 ) → ( ( ∃ 𝑎 ∃ 𝑏 ( ⟨ 𝑚 , 𝑛 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜑 ) → ⟨ 𝑚 , 𝑛 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ) → ⟨ 𝑚 , 𝑛 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ) )
91 oppr ⊢ ( ( 𝑚 ∈ V ∧ 𝑛 ∈ V ) → ( ⟨ 𝑚 , 𝑛 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ → { 𝑚 , 𝑛 } = { 𝑥 , 𝑦 } ) )
92 91 el2v ⊢ ( ⟨ 𝑚 , 𝑛 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ → { 𝑚 , 𝑛 } = { 𝑥 , 𝑦 } )
93 90 92 syl6 ⊢ ( ( ( ( 𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑋 ) ∧ ( 𝑚 = 𝑎 ∧ 𝑛 = 𝑏 ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ 𝜑 ) → ( ( ∃ 𝑎 ∃ 𝑏 ( ⟨ 𝑚 , 𝑛 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜑 ) → ⟨ 𝑚 , 𝑛 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ) → { 𝑚 , 𝑛 } = { 𝑥 , 𝑦 } ) )
94 93 ex ⊢ ( ( ( 𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑋 ) ∧ ( 𝑚 = 𝑎 ∧ 𝑛 = 𝑏 ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( 𝜑 → ( ( ∃ 𝑎 ∃ 𝑏 ( ⟨ 𝑚 , 𝑛 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜑 ) → ⟨ 𝑚 , 𝑛 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ) → { 𝑚 , 𝑛 } = { 𝑥 , 𝑦 } ) ) )
95 94 com23 ⊢ ( ( ( 𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑋 ) ∧ ( 𝑚 = 𝑎 ∧ 𝑛 = 𝑏 ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( ( ∃ 𝑎 ∃ 𝑏 ( ⟨ 𝑚 , 𝑛 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜑 ) → ⟨ 𝑚 , 𝑛 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ) → ( 𝜑 → { 𝑚 , 𝑛 } = { 𝑥 , 𝑦 } ) ) )
96 95 3exp ⊢ ( ( 𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑋 ) → ( ( 𝑚 = 𝑎 ∧ 𝑛 = 𝑏 ) → ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( ( ∃ 𝑎 ∃ 𝑏 ( ⟨ 𝑚 , 𝑛 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜑 ) → ⟨ 𝑚 , 𝑛 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ) → ( 𝜑 → { 𝑚 , 𝑛 } = { 𝑥 , 𝑦 } ) ) ) ) )
97 96 com24 ⊢ ( ( 𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑋 ) → ( ( ∃ 𝑎 ∃ 𝑏 ( ⟨ 𝑚 , 𝑛 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜑 ) → ⟨ 𝑚 , 𝑛 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ) → ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( ( 𝑚 = 𝑎 ∧ 𝑛 = 𝑏 ) → ( 𝜑 → { 𝑚 , 𝑛 } = { 𝑥 , 𝑦 } ) ) ) ) )
98 61 97 syld ⊢ ( ( 𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑋 ) → ( ∀ 𝑖 ∈ 𝑋 ∀ 𝑗 ∈ 𝑋 ( ∃ 𝑎 ∃ 𝑏 ( ⟨ 𝑖 , 𝑗 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜑 ) → ⟨ 𝑖 , 𝑗 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ) → ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( ( 𝑚 = 𝑎 ∧ 𝑛 = 𝑏 ) → ( 𝜑 → { 𝑚 , 𝑛 } = { 𝑥 , 𝑦 } ) ) ) ) )
99 98 com13 ⊢ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( ∀ 𝑖 ∈ 𝑋 ∀ 𝑗 ∈ 𝑋 ( ∃ 𝑎 ∃ 𝑏 ( ⟨ 𝑖 , 𝑗 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜑 ) → ⟨ 𝑖 , 𝑗 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ) → ( ( 𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑋 ) → ( ( 𝑚 = 𝑎 ∧ 𝑛 = 𝑏 ) → ( 𝜑 → { 𝑚 , 𝑛 } = { 𝑥 , 𝑦 } ) ) ) ) )
100 99 a1d ⊢ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( ∃ 𝑎 ∃ 𝑏 ( ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜑 ) → ( ∀ 𝑖 ∈ 𝑋 ∀ 𝑗 ∈ 𝑋 ( ∃ 𝑎 ∃ 𝑏 ( ⟨ 𝑖 , 𝑗 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜑 ) → ⟨ 𝑖 , 𝑗 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ) → ( ( 𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑋 ) → ( ( 𝑚 = 𝑎 ∧ 𝑛 = 𝑏 ) → ( 𝜑 → { 𝑚 , 𝑛 } = { 𝑥 , 𝑦 } ) ) ) ) ) )
101 100 imp42 ⊢ ( ( ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ∧ ( ∃ 𝑎 ∃ 𝑏 ( ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜑 ) ∧ ∀ 𝑖 ∈ 𝑋 ∀ 𝑗 ∈ 𝑋 ( ∃ 𝑎 ∃ 𝑏 ( ⟨ 𝑖 , 𝑗 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜑 ) → ⟨ 𝑖 , 𝑗 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ) ) ) ∧ ( 𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑋 ) ) → ( ( 𝑚 = 𝑎 ∧ 𝑛 = 𝑏 ) → ( 𝜑 → { 𝑚 , 𝑛 } = { 𝑥 , 𝑦 } ) ) )
102 opeq1 ⊢ ( 𝑖 = 𝑛 → ⟨ 𝑖 , 𝑗 ⟩ = ⟨ 𝑛 , 𝑗 ⟩ )
103 102 eqeq1d ⊢ ( 𝑖 = 𝑛 → ( ⟨ 𝑖 , 𝑗 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ↔ ⟨ 𝑛 , 𝑗 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ) )
104 103 anbi1d ⊢ ( 𝑖 = 𝑛 → ( ( ⟨ 𝑖 , 𝑗 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜑 ) ↔ ( ⟨ 𝑛 , 𝑗 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜑 ) ) )
105 104 2exbidv ⊢ ( 𝑖 = 𝑛 → ( ∃ 𝑎 ∃ 𝑏 ( ⟨ 𝑖 , 𝑗 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜑 ) ↔ ∃ 𝑎 ∃ 𝑏 ( ⟨ 𝑛 , 𝑗 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜑 ) ) )
106 102 eqeq1d ⊢ ( 𝑖 = 𝑛 → ( ⟨ 𝑖 , 𝑗 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ↔ ⟨ 𝑛 , 𝑗 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ) )
107 105 106 imbi12d ⊢ ( 𝑖 = 𝑛 → ( ( ∃ 𝑎 ∃ 𝑏 ( ⟨ 𝑖 , 𝑗 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜑 ) → ⟨ 𝑖 , 𝑗 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ) ↔ ( ∃ 𝑎 ∃ 𝑏 ( ⟨ 𝑛 , 𝑗 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜑 ) → ⟨ 𝑛 , 𝑗 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ) ) )
108 opeq2 ⊢ ( 𝑗 = 𝑚 → ⟨ 𝑛 , 𝑗 ⟩ = ⟨ 𝑛 , 𝑚 ⟩ )
109 108 eqeq1d ⊢ ( 𝑗 = 𝑚 → ( ⟨ 𝑛 , 𝑗 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ↔ ⟨ 𝑛 , 𝑚 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ) )
110 109 anbi1d ⊢ ( 𝑗 = 𝑚 → ( ( ⟨ 𝑛 , 𝑗 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜑 ) ↔ ( ⟨ 𝑛 , 𝑚 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜑 ) ) )
111 110 2exbidv ⊢ ( 𝑗 = 𝑚 → ( ∃ 𝑎 ∃ 𝑏 ( ⟨ 𝑛 , 𝑗 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜑 ) ↔ ∃ 𝑎 ∃ 𝑏 ( ⟨ 𝑛 , 𝑚 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜑 ) ) )
112 108 eqeq1d ⊢ ( 𝑗 = 𝑚 → ( ⟨ 𝑛 , 𝑗 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ↔ ⟨ 𝑛 , 𝑚 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ) )
113 111 112 imbi12d ⊢ ( 𝑗 = 𝑚 → ( ( ∃ 𝑎 ∃ 𝑏 ( ⟨ 𝑛 , 𝑗 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜑 ) → ⟨ 𝑛 , 𝑗 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ) ↔ ( ∃ 𝑎 ∃ 𝑏 ( ⟨ 𝑛 , 𝑚 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜑 ) → ⟨ 𝑛 , 𝑚 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ) ) )
114 107 113 rspc2v ⊢ ( ( 𝑛 ∈ 𝑋 ∧ 𝑚 ∈ 𝑋 ) → ( ∀ 𝑖 ∈ 𝑋 ∀ 𝑗 ∈ 𝑋 ( ∃ 𝑎 ∃ 𝑏 ( ⟨ 𝑖 , 𝑗 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜑 ) → ⟨ 𝑖 , 𝑗 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ) → ( ∃ 𝑎 ∃ 𝑏 ( ⟨ 𝑛 , 𝑚 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜑 ) → ⟨ 𝑛 , 𝑚 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ) ) )
115 114 ancoms ⊢ ( ( 𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑋 ) → ( ∀ 𝑖 ∈ 𝑋 ∀ 𝑗 ∈ 𝑋 ( ∃ 𝑎 ∃ 𝑏 ( ⟨ 𝑖 , 𝑗 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜑 ) → ⟨ 𝑖 , 𝑗 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ) → ( ∃ 𝑎 ∃ 𝑏 ( ⟨ 𝑛 , 𝑚 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜑 ) → ⟨ 𝑛 , 𝑚 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ) ) )
116 pm3.22 ⊢ ( ( 𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑋 ) → ( 𝑛 ∈ 𝑋 ∧ 𝑚 ∈ 𝑋 ) )
117 116 anim1ci ⊢ ( ( ( 𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑋 ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝑛 ∈ 𝑋 ∧ 𝑚 ∈ 𝑋 ) ) )
118 117 3adant2 ⊢ ( ( ( 𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑋 ) ∧ ( 𝑚 = 𝑏 ∧ 𝑛 = 𝑎 ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝑛 ∈ 𝑋 ∧ 𝑚 ∈ 𝑋 ) ) )
119 118 adantr ⊢ ( ( ( ( 𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑋 ) ∧ ( 𝑚 = 𝑏 ∧ 𝑛 = 𝑎 ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ 𝜑 ) → ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝑛 ∈ 𝑋 ∧ 𝑚 ∈ 𝑋 ) ) )
120 eqidd ⊢ ( ( ( ( 𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑋 ) ∧ ( 𝑚 = 𝑏 ∧ 𝑛 = 𝑎 ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ 𝜑 ) → ⟨ 𝑛 , 𝑚 ⟩ = ⟨ 𝑛 , 𝑚 ⟩ )
121 sbceq1a ⊢ ( 𝑏 = 𝑚 → ( 𝜑 ↔ [ 𝑚 / 𝑏 ] 𝜑 ) )
122 121 equcoms ⊢ ( 𝑚 = 𝑏 → ( 𝜑 ↔ [ 𝑚 / 𝑏 ] 𝜑 ) )
123 sbceq1a ⊢ ( 𝑎 = 𝑛 → ( [ 𝑚 / 𝑏 ] 𝜑 ↔ [ 𝑛 / 𝑎 ] [ 𝑚 / 𝑏 ] 𝜑 ) )
124 123 equcoms ⊢ ( 𝑛 = 𝑎 → ( [ 𝑚 / 𝑏 ] 𝜑 ↔ [ 𝑛 / 𝑎 ] [ 𝑚 / 𝑏 ] 𝜑 ) )
125 122 124 sylan9bb ⊢ ( ( 𝑚 = 𝑏 ∧ 𝑛 = 𝑎 ) → ( 𝜑 ↔ [ 𝑛 / 𝑎 ] [ 𝑚 / 𝑏 ] 𝜑 ) )
126 125 3ad2ant2 ⊢ ( ( ( 𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑋 ) ∧ ( 𝑚 = 𝑏 ∧ 𝑛 = 𝑎 ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( 𝜑 ↔ [ 𝑛 / 𝑎 ] [ 𝑚 / 𝑏 ] 𝜑 ) )
127 126 biimpa ⊢ ( ( ( ( 𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑋 ) ∧ ( 𝑚 = 𝑏 ∧ 𝑛 = 𝑎 ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ 𝜑 ) → [ 𝑛 / 𝑎 ] [ 𝑚 / 𝑏 ] 𝜑 )
128 119 120 127 jca32 ⊢ ( ( ( ( 𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑋 ) ∧ ( 𝑚 = 𝑏 ∧ 𝑛 = 𝑎 ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ 𝜑 ) → ( ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝑛 ∈ 𝑋 ∧ 𝑚 ∈ 𝑋 ) ) ∧ ( ⟨ 𝑛 , 𝑚 ⟩ = ⟨ 𝑛 , 𝑚 ⟩ ∧ [ 𝑛 / 𝑎 ] [ 𝑚 / 𝑏 ] 𝜑 ) ) )
129 nfv ⊢ Ⅎ 𝑎 ⟨ 𝑛 , 𝑚 ⟩ = ⟨ 𝑛 , 𝑚 ⟩
130 nfsbc1v ⊢ Ⅎ 𝑎 [ 𝑛 / 𝑎 ] [ 𝑚 / 𝑏 ] 𝜑
131 129 130 nfan ⊢ Ⅎ 𝑎 ( ⟨ 𝑛 , 𝑚 ⟩ = ⟨ 𝑛 , 𝑚 ⟩ ∧ [ 𝑛 / 𝑎 ] [ 𝑚 / 𝑏 ] 𝜑 )
132 nfv ⊢ Ⅎ 𝑏 ⟨ 𝑛 , 𝑚 ⟩ = ⟨ 𝑛 , 𝑚 ⟩
133 nfcv ⊢ Ⅎ 𝑏 𝑛
134 nfsbc1v ⊢ Ⅎ 𝑏 [ 𝑚 / 𝑏 ] 𝜑
135 133 134 nfsbcw ⊢ Ⅎ 𝑏 [ 𝑛 / 𝑎 ] [ 𝑚 / 𝑏 ] 𝜑
136 132 135 nfan ⊢ Ⅎ 𝑏 ( ⟨ 𝑛 , 𝑚 ⟩ = ⟨ 𝑛 , 𝑚 ⟩ ∧ [ 𝑛 / 𝑎 ] [ 𝑚 / 𝑏 ] 𝜑 )
137 opeq12 ⊢ ( ( 𝑎 = 𝑛 ∧ 𝑏 = 𝑚 ) → ⟨ 𝑎 , 𝑏 ⟩ = ⟨ 𝑛 , 𝑚 ⟩ )
138 137 eqeq2d ⊢ ( ( 𝑎 = 𝑛 ∧ 𝑏 = 𝑚 ) → ( ⟨ 𝑛 , 𝑚 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ↔ ⟨ 𝑛 , 𝑚 ⟩ = ⟨ 𝑛 , 𝑚 ⟩ ) )
139 121 123 sylan9bbr ⊢ ( ( 𝑎 = 𝑛 ∧ 𝑏 = 𝑚 ) → ( 𝜑 ↔ [ 𝑛 / 𝑎 ] [ 𝑚 / 𝑏 ] 𝜑 ) )
140 138 139 anbi12d ⊢ ( ( 𝑎 = 𝑛 ∧ 𝑏 = 𝑚 ) → ( ( ⟨ 𝑛 , 𝑚 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜑 ) ↔ ( ⟨ 𝑛 , 𝑚 ⟩ = ⟨ 𝑛 , 𝑚 ⟩ ∧ [ 𝑛 / 𝑎 ] [ 𝑚 / 𝑏 ] 𝜑 ) ) )
141 140 adantl ⊢ ( ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝑎 = 𝑛 ∧ 𝑏 = 𝑚 ) ) → ( ( ⟨ 𝑛 , 𝑚 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜑 ) ↔ ( ⟨ 𝑛 , 𝑚 ⟩ = ⟨ 𝑛 , 𝑚 ⟩ ∧ [ 𝑛 / 𝑎 ] [ 𝑚 / 𝑏 ] 𝜑 ) ) )
142 131 136 141 spc2ed ⊢ ( ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝑛 ∈ 𝑋 ∧ 𝑚 ∈ 𝑋 ) ) → ( ( ⟨ 𝑛 , 𝑚 ⟩ = ⟨ 𝑛 , 𝑚 ⟩ ∧ [ 𝑛 / 𝑎 ] [ 𝑚 / 𝑏 ] 𝜑 ) → ∃ 𝑎 ∃ 𝑏 ( ⟨ 𝑛 , 𝑚 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜑 ) ) )
143 142 imp ⊢ ( ( ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝑛 ∈ 𝑋 ∧ 𝑚 ∈ 𝑋 ) ) ∧ ( ⟨ 𝑛 , 𝑚 ⟩ = ⟨ 𝑛 , 𝑚 ⟩ ∧ [ 𝑛 / 𝑎 ] [ 𝑚 / 𝑏 ] 𝜑 ) ) → ∃ 𝑎 ∃ 𝑏 ( ⟨ 𝑛 , 𝑚 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜑 ) )
144 pm2.27 ⊢ ( ∃ 𝑎 ∃ 𝑏 ( ⟨ 𝑛 , 𝑚 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜑 ) → ( ( ∃ 𝑎 ∃ 𝑏 ( ⟨ 𝑛 , 𝑚 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜑 ) → ⟨ 𝑛 , 𝑚 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ) → ⟨ 𝑛 , 𝑚 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ) )
145 128 143 144 3syl ⊢ ( ( ( ( 𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑋 ) ∧ ( 𝑚 = 𝑏 ∧ 𝑛 = 𝑎 ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ 𝜑 ) → ( ( ∃ 𝑎 ∃ 𝑏 ( ⟨ 𝑛 , 𝑚 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜑 ) → ⟨ 𝑛 , 𝑚 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ) → ⟨ 𝑛 , 𝑚 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ) )
146 prcom ⊢ { 𝑛 , 𝑚 } = { 𝑚 , 𝑛 }
147 oppr ⊢ ( ( 𝑛 ∈ V ∧ 𝑚 ∈ V ) → ( ⟨ 𝑛 , 𝑚 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ → { 𝑛 , 𝑚 } = { 𝑥 , 𝑦 } ) )
148 147 el2v ⊢ ( ⟨ 𝑛 , 𝑚 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ → { 𝑛 , 𝑚 } = { 𝑥 , 𝑦 } )
149 146 148 eqtr3id ⊢ ( ⟨ 𝑛 , 𝑚 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ → { 𝑚 , 𝑛 } = { 𝑥 , 𝑦 } )
150 145 149 syl6 ⊢ ( ( ( ( 𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑋 ) ∧ ( 𝑚 = 𝑏 ∧ 𝑛 = 𝑎 ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ 𝜑 ) → ( ( ∃ 𝑎 ∃ 𝑏 ( ⟨ 𝑛 , 𝑚 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜑 ) → ⟨ 𝑛 , 𝑚 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ) → { 𝑚 , 𝑛 } = { 𝑥 , 𝑦 } ) )
151 150 ex ⊢ ( ( ( 𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑋 ) ∧ ( 𝑚 = 𝑏 ∧ 𝑛 = 𝑎 ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( 𝜑 → ( ( ∃ 𝑎 ∃ 𝑏 ( ⟨ 𝑛 , 𝑚 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜑 ) → ⟨ 𝑛 , 𝑚 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ) → { 𝑚 , 𝑛 } = { 𝑥 , 𝑦 } ) ) )
152 151 com23 ⊢ ( ( ( 𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑋 ) ∧ ( 𝑚 = 𝑏 ∧ 𝑛 = 𝑎 ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( ( ∃ 𝑎 ∃ 𝑏 ( ⟨ 𝑛 , 𝑚 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜑 ) → ⟨ 𝑛 , 𝑚 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ) → ( 𝜑 → { 𝑚 , 𝑛 } = { 𝑥 , 𝑦 } ) ) )
153 152 3exp ⊢ ( ( 𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑋 ) → ( ( 𝑚 = 𝑏 ∧ 𝑛 = 𝑎 ) → ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( ( ∃ 𝑎 ∃ 𝑏 ( ⟨ 𝑛 , 𝑚 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜑 ) → ⟨ 𝑛 , 𝑚 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ) → ( 𝜑 → { 𝑚 , 𝑛 } = { 𝑥 , 𝑦 } ) ) ) ) )
154 153 com24 ⊢ ( ( 𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑋 ) → ( ( ∃ 𝑎 ∃ 𝑏 ( ⟨ 𝑛 , 𝑚 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜑 ) → ⟨ 𝑛 , 𝑚 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ) → ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( ( 𝑚 = 𝑏 ∧ 𝑛 = 𝑎 ) → ( 𝜑 → { 𝑚 , 𝑛 } = { 𝑥 , 𝑦 } ) ) ) ) )
155 115 154 syld ⊢ ( ( 𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑋 ) → ( ∀ 𝑖 ∈ 𝑋 ∀ 𝑗 ∈ 𝑋 ( ∃ 𝑎 ∃ 𝑏 ( ⟨ 𝑖 , 𝑗 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜑 ) → ⟨ 𝑖 , 𝑗 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ) → ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( ( 𝑚 = 𝑏 ∧ 𝑛 = 𝑎 ) → ( 𝜑 → { 𝑚 , 𝑛 } = { 𝑥 , 𝑦 } ) ) ) ) )
156 155 com13 ⊢ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( ∀ 𝑖 ∈ 𝑋 ∀ 𝑗 ∈ 𝑋 ( ∃ 𝑎 ∃ 𝑏 ( ⟨ 𝑖 , 𝑗 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜑 ) → ⟨ 𝑖 , 𝑗 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ) → ( ( 𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑋 ) → ( ( 𝑚 = 𝑏 ∧ 𝑛 = 𝑎 ) → ( 𝜑 → { 𝑚 , 𝑛 } = { 𝑥 , 𝑦 } ) ) ) ) )
157 156 a1d ⊢ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( ∃ 𝑎 ∃ 𝑏 ( ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜑 ) → ( ∀ 𝑖 ∈ 𝑋 ∀ 𝑗 ∈ 𝑋 ( ∃ 𝑎 ∃ 𝑏 ( ⟨ 𝑖 , 𝑗 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜑 ) → ⟨ 𝑖 , 𝑗 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ) → ( ( 𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑋 ) → ( ( 𝑚 = 𝑏 ∧ 𝑛 = 𝑎 ) → ( 𝜑 → { 𝑚 , 𝑛 } = { 𝑥 , 𝑦 } ) ) ) ) ) )
158 157 imp42 ⊢ ( ( ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ∧ ( ∃ 𝑎 ∃ 𝑏 ( ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜑 ) ∧ ∀ 𝑖 ∈ 𝑋 ∀ 𝑗 ∈ 𝑋 ( ∃ 𝑎 ∃ 𝑏 ( ⟨ 𝑖 , 𝑗 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜑 ) → ⟨ 𝑖 , 𝑗 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ) ) ) ∧ ( 𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑋 ) ) → ( ( 𝑚 = 𝑏 ∧ 𝑛 = 𝑎 ) → ( 𝜑 → { 𝑚 , 𝑛 } = { 𝑥 , 𝑦 } ) ) )
159 101 158 jaod ⊢ ( ( ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ∧ ( ∃ 𝑎 ∃ 𝑏 ( ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜑 ) ∧ ∀ 𝑖 ∈ 𝑋 ∀ 𝑗 ∈ 𝑋 ( ∃ 𝑎 ∃ 𝑏 ( ⟨ 𝑖 , 𝑗 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜑 ) → ⟨ 𝑖 , 𝑗 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ) ) ) ∧ ( 𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑋 ) ) → ( ( ( 𝑚 = 𝑎 ∧ 𝑛 = 𝑏 ) ∨ ( 𝑚 = 𝑏 ∧ 𝑛 = 𝑎 ) ) → ( 𝜑 → { 𝑚 , 𝑛 } = { 𝑥 , 𝑦 } ) ) )
160 48 159 biimtrid ⊢ ( ( ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ∧ ( ∃ 𝑎 ∃ 𝑏 ( ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜑 ) ∧ ∀ 𝑖 ∈ 𝑋 ∀ 𝑗 ∈ 𝑋 ( ∃ 𝑎 ∃ 𝑏 ( ⟨ 𝑖 , 𝑗 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜑 ) → ⟨ 𝑖 , 𝑗 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ) ) ) ∧ ( 𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑋 ) ) → ( { 𝑚 , 𝑛 } = { 𝑎 , 𝑏 } → ( 𝜑 → { 𝑚 , 𝑛 } = { 𝑥 , 𝑦 } ) ) )
161 160 impd ⊢ ( ( ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ∧ ( ∃ 𝑎 ∃ 𝑏 ( ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜑 ) ∧ ∀ 𝑖 ∈ 𝑋 ∀ 𝑗 ∈ 𝑋 ( ∃ 𝑎 ∃ 𝑏 ( ⟨ 𝑖 , 𝑗 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜑 ) → ⟨ 𝑖 , 𝑗 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ) ) ) ∧ ( 𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑋 ) ) → ( ( { 𝑚 , 𝑛 } = { 𝑎 , 𝑏 } ∧ 𝜑 ) → { 𝑚 , 𝑛 } = { 𝑥 , 𝑦 } ) )
162 42 43 161 exlimd ⊢ ( ( ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ∧ ( ∃ 𝑎 ∃ 𝑏 ( ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜑 ) ∧ ∀ 𝑖 ∈ 𝑋 ∀ 𝑗 ∈ 𝑋 ( ∃ 𝑎 ∃ 𝑏 ( ⟨ 𝑖 , 𝑗 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜑 ) → ⟨ 𝑖 , 𝑗 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ) ) ) ∧ ( 𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑋 ) ) → ( ∃ 𝑏 ( { 𝑚 , 𝑛 } = { 𝑎 , 𝑏 } ∧ 𝜑 ) → { 𝑚 , 𝑛 } = { 𝑥 , 𝑦 } ) )
163 27 28 162 exlimd ⊢ ( ( ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ∧ ( ∃ 𝑎 ∃ 𝑏 ( ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜑 ) ∧ ∀ 𝑖 ∈ 𝑋 ∀ 𝑗 ∈ 𝑋 ( ∃ 𝑎 ∃ 𝑏 ( ⟨ 𝑖 , 𝑗 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜑 ) → ⟨ 𝑖 , 𝑗 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ) ) ) ∧ ( 𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑋 ) ) → ( ∃ 𝑎 ∃ 𝑏 ( { 𝑚 , 𝑛 } = { 𝑎 , 𝑏 } ∧ 𝜑 ) → { 𝑚 , 𝑛 } = { 𝑥 , 𝑦 } ) )
164 163 ralrimivva ⊢ ( ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ∧ ( ∃ 𝑎 ∃ 𝑏 ( ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜑 ) ∧ ∀ 𝑖 ∈ 𝑋 ∀ 𝑗 ∈ 𝑋 ( ∃ 𝑎 ∃ 𝑏 ( ⟨ 𝑖 , 𝑗 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜑 ) → ⟨ 𝑖 , 𝑗 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ) ) ) → ∀ 𝑚 ∈ 𝑋 ∀ 𝑛 ∈ 𝑋 ( ∃ 𝑎 ∃ 𝑏 ( { 𝑚 , 𝑛 } = { 𝑎 , 𝑏 } ∧ 𝜑 ) → { 𝑚 , 𝑛 } = { 𝑥 , 𝑦 } ) )
165 preq1 ⊢ ( 𝑣 = 𝑥 → { 𝑣 , 𝑤 } = { 𝑥 , 𝑤 } )
166 165 eqeq1d ⊢ ( 𝑣 = 𝑥 → ( { 𝑣 , 𝑤 } = { 𝑎 , 𝑏 } ↔ { 𝑥 , 𝑤 } = { 𝑎 , 𝑏 } ) )
167 166 anbi1d ⊢ ( 𝑣 = 𝑥 → ( ( { 𝑣 , 𝑤 } = { 𝑎 , 𝑏 } ∧ 𝜑 ) ↔ ( { 𝑥 , 𝑤 } = { 𝑎 , 𝑏 } ∧ 𝜑 ) ) )
168 167 2exbidv ⊢ ( 𝑣 = 𝑥 → ( ∃ 𝑎 ∃ 𝑏 ( { 𝑣 , 𝑤 } = { 𝑎 , 𝑏 } ∧ 𝜑 ) ↔ ∃ 𝑎 ∃ 𝑏 ( { 𝑥 , 𝑤 } = { 𝑎 , 𝑏 } ∧ 𝜑 ) ) )
169 165 eqeq2d ⊢ ( 𝑣 = 𝑥 → ( { 𝑚 , 𝑛 } = { 𝑣 , 𝑤 } ↔ { 𝑚 , 𝑛 } = { 𝑥 , 𝑤 } ) )
170 169 imbi2d ⊢ ( 𝑣 = 𝑥 → ( ( ∃ 𝑎 ∃ 𝑏 ( { 𝑚 , 𝑛 } = { 𝑎 , 𝑏 } ∧ 𝜑 ) → { 𝑚 , 𝑛 } = { 𝑣 , 𝑤 } ) ↔ ( ∃ 𝑎 ∃ 𝑏 ( { 𝑚 , 𝑛 } = { 𝑎 , 𝑏 } ∧ 𝜑 ) → { 𝑚 , 𝑛 } = { 𝑥 , 𝑤 } ) ) )
171 170 2ralbidv ⊢ ( 𝑣 = 𝑥 → ( ∀ 𝑚 ∈ 𝑋 ∀ 𝑛 ∈ 𝑋 ( ∃ 𝑎 ∃ 𝑏 ( { 𝑚 , 𝑛 } = { 𝑎 , 𝑏 } ∧ 𝜑 ) → { 𝑚 , 𝑛 } = { 𝑣 , 𝑤 } ) ↔ ∀ 𝑚 ∈ 𝑋 ∀ 𝑛 ∈ 𝑋 ( ∃ 𝑎 ∃ 𝑏 ( { 𝑚 , 𝑛 } = { 𝑎 , 𝑏 } ∧ 𝜑 ) → { 𝑚 , 𝑛 } = { 𝑥 , 𝑤 } ) ) )
172 168 171 anbi12d ⊢ ( 𝑣 = 𝑥 → ( ( ∃ 𝑎 ∃ 𝑏 ( { 𝑣 , 𝑤 } = { 𝑎 , 𝑏 } ∧ 𝜑 ) ∧ ∀ 𝑚 ∈ 𝑋 ∀ 𝑛 ∈ 𝑋 ( ∃ 𝑎 ∃ 𝑏 ( { 𝑚 , 𝑛 } = { 𝑎 , 𝑏 } ∧ 𝜑 ) → { 𝑚 , 𝑛 } = { 𝑣 , 𝑤 } ) ) ↔ ( ∃ 𝑎 ∃ 𝑏 ( { 𝑥 , 𝑤 } = { 𝑎 , 𝑏 } ∧ 𝜑 ) ∧ ∀ 𝑚 ∈ 𝑋 ∀ 𝑛 ∈ 𝑋 ( ∃ 𝑎 ∃ 𝑏 ( { 𝑚 , 𝑛 } = { 𝑎 , 𝑏 } ∧ 𝜑 ) → { 𝑚 , 𝑛 } = { 𝑥 , 𝑤 } ) ) ) )
173 preq2 ⊢ ( 𝑤 = 𝑦 → { 𝑥 , 𝑤 } = { 𝑥 , 𝑦 } )
174 173 eqeq1d ⊢ ( 𝑤 = 𝑦 → ( { 𝑥 , 𝑤 } = { 𝑎 , 𝑏 } ↔ { 𝑥 , 𝑦 } = { 𝑎 , 𝑏 } ) )
175 174 anbi1d ⊢ ( 𝑤 = 𝑦 → ( ( { 𝑥 , 𝑤 } = { 𝑎 , 𝑏 } ∧ 𝜑 ) ↔ ( { 𝑥 , 𝑦 } = { 𝑎 , 𝑏 } ∧ 𝜑 ) ) )
176 175 2exbidv ⊢ ( 𝑤 = 𝑦 → ( ∃ 𝑎 ∃ 𝑏 ( { 𝑥 , 𝑤 } = { 𝑎 , 𝑏 } ∧ 𝜑 ) ↔ ∃ 𝑎 ∃ 𝑏 ( { 𝑥 , 𝑦 } = { 𝑎 , 𝑏 } ∧ 𝜑 ) ) )
177 173 eqeq2d ⊢ ( 𝑤 = 𝑦 → ( { 𝑚 , 𝑛 } = { 𝑥 , 𝑤 } ↔ { 𝑚 , 𝑛 } = { 𝑥 , 𝑦 } ) )
178 177 imbi2d ⊢ ( 𝑤 = 𝑦 → ( ( ∃ 𝑎 ∃ 𝑏 ( { 𝑚 , 𝑛 } = { 𝑎 , 𝑏 } ∧ 𝜑 ) → { 𝑚 , 𝑛 } = { 𝑥 , 𝑤 } ) ↔ ( ∃ 𝑎 ∃ 𝑏 ( { 𝑚 , 𝑛 } = { 𝑎 , 𝑏 } ∧ 𝜑 ) → { 𝑚 , 𝑛 } = { 𝑥 , 𝑦 } ) ) )
179 178 2ralbidv ⊢ ( 𝑤 = 𝑦 → ( ∀ 𝑚 ∈ 𝑋 ∀ 𝑛 ∈ 𝑋 ( ∃ 𝑎 ∃ 𝑏 ( { 𝑚 , 𝑛 } = { 𝑎 , 𝑏 } ∧ 𝜑 ) → { 𝑚 , 𝑛 } = { 𝑥 , 𝑤 } ) ↔ ∀ 𝑚 ∈ 𝑋 ∀ 𝑛 ∈ 𝑋 ( ∃ 𝑎 ∃ 𝑏 ( { 𝑚 , 𝑛 } = { 𝑎 , 𝑏 } ∧ 𝜑 ) → { 𝑚 , 𝑛 } = { 𝑥 , 𝑦 } ) ) )
180 176 179 anbi12d ⊢ ( 𝑤 = 𝑦 → ( ( ∃ 𝑎 ∃ 𝑏 ( { 𝑥 , 𝑤 } = { 𝑎 , 𝑏 } ∧ 𝜑 ) ∧ ∀ 𝑚 ∈ 𝑋 ∀ 𝑛 ∈ 𝑋 ( ∃ 𝑎 ∃ 𝑏 ( { 𝑚 , 𝑛 } = { 𝑎 , 𝑏 } ∧ 𝜑 ) → { 𝑚 , 𝑛 } = { 𝑥 , 𝑤 } ) ) ↔ ( ∃ 𝑎 ∃ 𝑏 ( { 𝑥 , 𝑦 } = { 𝑎 , 𝑏 } ∧ 𝜑 ) ∧ ∀ 𝑚 ∈ 𝑋 ∀ 𝑛 ∈ 𝑋 ( ∃ 𝑎 ∃ 𝑏 ( { 𝑚 , 𝑛 } = { 𝑎 , 𝑏 } ∧ 𝜑 ) → { 𝑚 , 𝑛 } = { 𝑥 , 𝑦 } ) ) ) )
181 172 180 rspc2ev ⊢ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ ( ∃ 𝑎 ∃ 𝑏 ( { 𝑥 , 𝑦 } = { 𝑎 , 𝑏 } ∧ 𝜑 ) ∧ ∀ 𝑚 ∈ 𝑋 ∀ 𝑛 ∈ 𝑋 ( ∃ 𝑎 ∃ 𝑏 ( { 𝑚 , 𝑛 } = { 𝑎 , 𝑏 } ∧ 𝜑 ) → { 𝑚 , 𝑛 } = { 𝑥 , 𝑦 } ) ) ) → ∃ 𝑣 ∈ 𝑋 ∃ 𝑤 ∈ 𝑋 ( ∃ 𝑎 ∃ 𝑏 ( { 𝑣 , 𝑤 } = { 𝑎 , 𝑏 } ∧ 𝜑 ) ∧ ∀ 𝑚 ∈ 𝑋 ∀ 𝑛 ∈ 𝑋 ( ∃ 𝑎 ∃ 𝑏 ( { 𝑚 , 𝑛 } = { 𝑎 , 𝑏 } ∧ 𝜑 ) → { 𝑚 , 𝑛 } = { 𝑣 , 𝑤 } ) ) )
182 8 9 15 164 181 syl112anc ⊢ ( ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ∧ ( ∃ 𝑎 ∃ 𝑏 ( ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜑 ) ∧ ∀ 𝑖 ∈ 𝑋 ∀ 𝑗 ∈ 𝑋 ( ∃ 𝑎 ∃ 𝑏 ( ⟨ 𝑖 , 𝑗 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜑 ) → ⟨ 𝑖 , 𝑗 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ) ) ) → ∃ 𝑣 ∈ 𝑋 ∃ 𝑤 ∈ 𝑋 ( ∃ 𝑎 ∃ 𝑏 ( { 𝑣 , 𝑤 } = { 𝑎 , 𝑏 } ∧ 𝜑 ) ∧ ∀ 𝑚 ∈ 𝑋 ∀ 𝑛 ∈ 𝑋 ( ∃ 𝑎 ∃ 𝑏 ( { 𝑚 , 𝑛 } = { 𝑎 , 𝑏 } ∧ 𝜑 ) → { 𝑚 , 𝑛 } = { 𝑣 , 𝑤 } ) ) )
183 182 ex ⊢ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( ( ∃ 𝑎 ∃ 𝑏 ( ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜑 ) ∧ ∀ 𝑖 ∈ 𝑋 ∀ 𝑗 ∈ 𝑋 ( ∃ 𝑎 ∃ 𝑏 ( ⟨ 𝑖 , 𝑗 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜑 ) → ⟨ 𝑖 , 𝑗 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ) ) → ∃ 𝑣 ∈ 𝑋 ∃ 𝑤 ∈ 𝑋 ( ∃ 𝑎 ∃ 𝑏 ( { 𝑣 , 𝑤 } = { 𝑎 , 𝑏 } ∧ 𝜑 ) ∧ ∀ 𝑚 ∈ 𝑋 ∀ 𝑛 ∈ 𝑋 ( ∃ 𝑎 ∃ 𝑏 ( { 𝑚 , 𝑛 } = { 𝑎 , 𝑏 } ∧ 𝜑 ) → { 𝑚 , 𝑛 } = { 𝑣 , 𝑤 } ) ) ) )
184 183 rexlimivv ⊢ ( ∃ 𝑥 ∈ 𝑋 ∃ 𝑦 ∈ 𝑋 ( ∃ 𝑎 ∃ 𝑏 ( ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜑 ) ∧ ∀ 𝑖 ∈ 𝑋 ∀ 𝑗 ∈ 𝑋 ( ∃ 𝑎 ∃ 𝑏 ( ⟨ 𝑖 , 𝑗 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜑 ) → ⟨ 𝑖 , 𝑗 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ) ) → ∃ 𝑣 ∈ 𝑋 ∃ 𝑤 ∈ 𝑋 ( ∃ 𝑎 ∃ 𝑏 ( { 𝑣 , 𝑤 } = { 𝑎 , 𝑏 } ∧ 𝜑 ) ∧ ∀ 𝑚 ∈ 𝑋 ∀ 𝑛 ∈ 𝑋 ( ∃ 𝑎 ∃ 𝑏 ( { 𝑚 , 𝑛 } = { 𝑎 , 𝑏 } ∧ 𝜑 ) → { 𝑚 , 𝑛 } = { 𝑣 , 𝑤 } ) ) )
185 eqeq1 ⊢ ( 𝑝 = { 𝑣 , 𝑤 } → ( 𝑝 = { 𝑎 , 𝑏 } ↔ { 𝑣 , 𝑤 } = { 𝑎 , 𝑏 } ) )
186 185 anbi1d ⊢ ( 𝑝 = { 𝑣 , 𝑤 } → ( ( 𝑝 = { 𝑎 , 𝑏 } ∧ 𝜑 ) ↔ ( { 𝑣 , 𝑤 } = { 𝑎 , 𝑏 } ∧ 𝜑 ) ) )
187 186 2exbidv ⊢ ( 𝑝 = { 𝑣 , 𝑤 } → ( ∃ 𝑎 ∃ 𝑏 ( 𝑝 = { 𝑎 , 𝑏 } ∧ 𝜑 ) ↔ ∃ 𝑎 ∃ 𝑏 ( { 𝑣 , 𝑤 } = { 𝑎 , 𝑏 } ∧ 𝜑 ) ) )
188 eqeq1 ⊢ ( 𝑝 = { 𝑚 , 𝑛 } → ( 𝑝 = { 𝑎 , 𝑏 } ↔ { 𝑚 , 𝑛 } = { 𝑎 , 𝑏 } ) )
189 188 anbi1d ⊢ ( 𝑝 = { 𝑚 , 𝑛 } → ( ( 𝑝 = { 𝑎 , 𝑏 } ∧ 𝜑 ) ↔ ( { 𝑚 , 𝑛 } = { 𝑎 , 𝑏 } ∧ 𝜑 ) ) )
190 189 2exbidv ⊢ ( 𝑝 = { 𝑚 , 𝑛 } → ( ∃ 𝑎 ∃ 𝑏 ( 𝑝 = { 𝑎 , 𝑏 } ∧ 𝜑 ) ↔ ∃ 𝑎 ∃ 𝑏 ( { 𝑚 , 𝑛 } = { 𝑎 , 𝑏 } ∧ 𝜑 ) ) )
191 187 190 reupr ⊢ ( 𝑋 ∈ 𝑉 → ( ∃! 𝑝 ∈ ( Pairs ‘ 𝑋 ) ∃ 𝑎 ∃ 𝑏 ( 𝑝 = { 𝑎 , 𝑏 } ∧ 𝜑 ) ↔ ∃ 𝑣 ∈ 𝑋 ∃ 𝑤 ∈ 𝑋 ( ∃ 𝑎 ∃ 𝑏 ( { 𝑣 , 𝑤 } = { 𝑎 , 𝑏 } ∧ 𝜑 ) ∧ ∀ 𝑚 ∈ 𝑋 ∀ 𝑛 ∈ 𝑋 ( ∃ 𝑎 ∃ 𝑏 ( { 𝑚 , 𝑛 } = { 𝑎 , 𝑏 } ∧ 𝜑 ) → { 𝑚 , 𝑛 } = { 𝑣 , 𝑤 } ) ) ) )
192 184 191 imbitrrid ⊢ ( 𝑋 ∈ 𝑉 → ( ∃ 𝑥 ∈ 𝑋 ∃ 𝑦 ∈ 𝑋 ( ∃ 𝑎 ∃ 𝑏 ( ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜑 ) ∧ ∀ 𝑖 ∈ 𝑋 ∀ 𝑗 ∈ 𝑋 ( ∃ 𝑎 ∃ 𝑏 ( ⟨ 𝑖 , 𝑗 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜑 ) → ⟨ 𝑖 , 𝑗 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ) ) → ∃! 𝑝 ∈ ( Pairs ‘ 𝑋 ) ∃ 𝑎 ∃ 𝑏 ( 𝑝 = { 𝑎 , 𝑏 } ∧ 𝜑 ) ) )
193 7 192 biimtrid ⊢ ( 𝑋 ∈ 𝑉 → ( ∃! 𝑝 ∈ ( 𝑋 × 𝑋 ) ∃ 𝑎 ∃ 𝑏 ( 𝑝 = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜑 ) → ∃! 𝑝 ∈ ( Pairs ‘ 𝑋 ) ∃ 𝑎 ∃ 𝑏 ( 𝑝 = { 𝑎 , 𝑏 } ∧ 𝜑 ) ) )