Metamath Proof Explorer

Theorem ichreuopeq

Description: If the setvar variables are interchangeable in a wff, and there is a unique ordered pair fulfilling the wff, then both setvar variables must be equal. (Contributed by AV, 28-Aug-2023)

Ref Expression
Assertion ichreuopeq ( [ 𝑎 ⇄ 𝑏 ] 𝜑 → ( ∃! 𝑝 ∈ ( 𝑋 × 𝑋 ) ∃ 𝑎 ∃ 𝑏 ( 𝑝 = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜑 ) → ∃ 𝑎 ∃ 𝑏 ( 𝑎 = 𝑏 ∧ 𝜑 ) ) )

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 nfich1 ⊢ Ⅎ 𝑎 [ 𝑎 ⇄ 𝑏 ] 𝜑
9 nfv ⊢ Ⅎ 𝑎 ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 )
10 8 9 nfan ⊢ Ⅎ 𝑎 ( [ 𝑎 ⇄ 𝑏 ] 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) )
11 nfcv ⊢ Ⅎ 𝑎 𝑋
12 nfe1 ⊢ Ⅎ 𝑎 ∃ 𝑎 ∃ 𝑏 ( ⟨ 𝑣 , 𝑤 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜑 )
13 nfv ⊢ Ⅎ 𝑎 ⟨ 𝑣 , 𝑤 ⟩ = ⟨ 𝑥 , 𝑦 ⟩
14 12 13 nfim ⊢ Ⅎ 𝑎 ( ∃ 𝑎 ∃ 𝑏 ( ⟨ 𝑣 , 𝑤 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜑 ) → ⟨ 𝑣 , 𝑤 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ )
15 11 14 nfralw ⊢ Ⅎ 𝑎 ∀ 𝑤 ∈ 𝑋 ( ∃ 𝑎 ∃ 𝑏 ( ⟨ 𝑣 , 𝑤 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜑 ) → ⟨ 𝑣 , 𝑤 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ )
16 11 15 nfralw ⊢ Ⅎ 𝑎 ∀ 𝑣 ∈ 𝑋 ∀ 𝑤 ∈ 𝑋 ( ∃ 𝑎 ∃ 𝑏 ( ⟨ 𝑣 , 𝑤 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜑 ) → ⟨ 𝑣 , 𝑤 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ )
17 nfe1 ⊢ Ⅎ 𝑎 ∃ 𝑎 ∃ 𝑏 ( 𝑎 = 𝑏 ∧ 𝜑 )
18 16 17 nfim ⊢ Ⅎ 𝑎 ( ∀ 𝑣 ∈ 𝑋 ∀ 𝑤 ∈ 𝑋 ( ∃ 𝑎 ∃ 𝑏 ( ⟨ 𝑣 , 𝑤 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜑 ) → ⟨ 𝑣 , 𝑤 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ) → ∃ 𝑎 ∃ 𝑏 ( 𝑎 = 𝑏 ∧ 𝜑 ) )
19 nfich2 ⊢ Ⅎ 𝑏 [ 𝑎 ⇄ 𝑏 ] 𝜑
20 nfv ⊢ Ⅎ 𝑏 ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 )
21 19 20 nfan ⊢ Ⅎ 𝑏 ( [ 𝑎 ⇄ 𝑏 ] 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) )
22 nfcv ⊢ Ⅎ 𝑏 𝑋
23 nfe1 ⊢ Ⅎ 𝑏 ∃ 𝑏 ( ⟨ 𝑣 , 𝑤 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜑 )
24 23 nfex ⊢ Ⅎ 𝑏 ∃ 𝑎 ∃ 𝑏 ( ⟨ 𝑣 , 𝑤 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜑 )
25 nfv ⊢ Ⅎ 𝑏 ⟨ 𝑣 , 𝑤 ⟩ = ⟨ 𝑥 , 𝑦 ⟩
26 24 25 nfim ⊢ Ⅎ 𝑏 ( ∃ 𝑎 ∃ 𝑏 ( ⟨ 𝑣 , 𝑤 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜑 ) → ⟨ 𝑣 , 𝑤 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ )
27 22 26 nfralw ⊢ Ⅎ 𝑏 ∀ 𝑤 ∈ 𝑋 ( ∃ 𝑎 ∃ 𝑏 ( ⟨ 𝑣 , 𝑤 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜑 ) → ⟨ 𝑣 , 𝑤 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ )
28 22 27 nfralw ⊢ Ⅎ 𝑏 ∀ 𝑣 ∈ 𝑋 ∀ 𝑤 ∈ 𝑋 ( ∃ 𝑎 ∃ 𝑏 ( ⟨ 𝑣 , 𝑤 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜑 ) → ⟨ 𝑣 , 𝑤 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ )
29 nfe1 ⊢ Ⅎ 𝑏 ∃ 𝑏 ( 𝑎 = 𝑏 ∧ 𝜑 )
30 29 nfex ⊢ Ⅎ 𝑏 ∃ 𝑎 ∃ 𝑏 ( 𝑎 = 𝑏 ∧ 𝜑 )
31 28 30 nfim ⊢ Ⅎ 𝑏 ( ∀ 𝑣 ∈ 𝑋 ∀ 𝑤 ∈ 𝑋 ( ∃ 𝑎 ∃ 𝑏 ( ⟨ 𝑣 , 𝑤 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜑 ) → ⟨ 𝑣 , 𝑤 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ) → ∃ 𝑎 ∃ 𝑏 ( 𝑎 = 𝑏 ∧ 𝜑 ) )
32 opeq12 ⊢ ( ( 𝑣 = 𝑦 ∧ 𝑤 = 𝑥 ) → ⟨ 𝑣 , 𝑤 ⟩ = ⟨ 𝑦 , 𝑥 ⟩ )
33 32 eqeq1d ⊢ ( ( 𝑣 = 𝑦 ∧ 𝑤 = 𝑥 ) → ( ⟨ 𝑣 , 𝑤 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ↔ ⟨ 𝑦 , 𝑥 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ) )
34 33 anbi1d ⊢ ( ( 𝑣 = 𝑦 ∧ 𝑤 = 𝑥 ) → ( ( ⟨ 𝑣 , 𝑤 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜑 ) ↔ ( ⟨ 𝑦 , 𝑥 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜑 ) ) )
35 34 2exbidv ⊢ ( ( 𝑣 = 𝑦 ∧ 𝑤 = 𝑥 ) → ( ∃ 𝑎 ∃ 𝑏 ( ⟨ 𝑣 , 𝑤 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜑 ) ↔ ∃ 𝑎 ∃ 𝑏 ( ⟨ 𝑦 , 𝑥 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜑 ) ) )
36 32 eqeq1d ⊢ ( ( 𝑣 = 𝑦 ∧ 𝑤 = 𝑥 ) → ( ⟨ 𝑣 , 𝑤 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ↔ ⟨ 𝑦 , 𝑥 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ) )
37 35 36 imbi12d ⊢ ( ( 𝑣 = 𝑦 ∧ 𝑤 = 𝑥 ) → ( ( ∃ 𝑎 ∃ 𝑏 ( ⟨ 𝑣 , 𝑤 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜑 ) → ⟨ 𝑣 , 𝑤 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ) ↔ ( ∃ 𝑎 ∃ 𝑏 ( ⟨ 𝑦 , 𝑥 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜑 ) → ⟨ 𝑦 , 𝑥 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ) ) )
38 37 rspc2gv ⊢ ( ( 𝑦 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ) → ( ∀ 𝑣 ∈ 𝑋 ∀ 𝑤 ∈ 𝑋 ( ∃ 𝑎 ∃ 𝑏 ( ⟨ 𝑣 , 𝑤 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜑 ) → ⟨ 𝑣 , 𝑤 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ) → ( ∃ 𝑎 ∃ 𝑏 ( ⟨ 𝑦 , 𝑥 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜑 ) → ⟨ 𝑦 , 𝑥 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ) ) )
39 38 ancoms ⊢ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( ∀ 𝑣 ∈ 𝑋 ∀ 𝑤 ∈ 𝑋 ( ∃ 𝑎 ∃ 𝑏 ( ⟨ 𝑣 , 𝑤 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜑 ) → ⟨ 𝑣 , 𝑤 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ) → ( ∃ 𝑎 ∃ 𝑏 ( ⟨ 𝑦 , 𝑥 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜑 ) → ⟨ 𝑦 , 𝑥 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ) ) )
40 39 adantl ⊢ ( ( [ 𝑎 ⇄ 𝑏 ] 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( ∀ 𝑣 ∈ 𝑋 ∀ 𝑤 ∈ 𝑋 ( ∃ 𝑎 ∃ 𝑏 ( ⟨ 𝑣 , 𝑤 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜑 ) → ⟨ 𝑣 , 𝑤 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ) → ( ∃ 𝑎 ∃ 𝑏 ( ⟨ 𝑦 , 𝑥 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜑 ) → ⟨ 𝑦 , 𝑥 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ) ) )
41 simprr ⊢ ( ( [ 𝑎 ⇄ 𝑏 ] 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → 𝑦 ∈ 𝑋 )
42 41 adantr ⊢ ( ( ( [ 𝑎 ⇄ 𝑏 ] 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ ( ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜑 ) ) → 𝑦 ∈ 𝑋 )
43 simpl ⊢ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → 𝑥 ∈ 𝑋 )
44 43 adantl ⊢ ( ( [ 𝑎 ⇄ 𝑏 ] 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → 𝑥 ∈ 𝑋 )
45 44 adantr ⊢ ( ( ( [ 𝑎 ⇄ 𝑏 ] 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ ( ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜑 ) ) → 𝑥 ∈ 𝑋 )
46 eqidd ⊢ ( ( ( [ 𝑎 ⇄ 𝑏 ] 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ ( ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜑 ) ) → ⟨ 𝑦 , 𝑥 ⟩ = ⟨ 𝑦 , 𝑥 ⟩ )
47 vex ⊢ 𝑥 ∈ V
48 vex ⊢ 𝑦 ∈ V
49 47 48 opth ⊢ ( ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ↔ ( 𝑥 = 𝑎 ∧ 𝑦 = 𝑏 ) )
50 sbceq1a ⊢ ( 𝑏 = 𝑦 → ( 𝜑 ↔ [ 𝑦 / 𝑏 ] 𝜑 ) )
51 50 equcoms ⊢ ( 𝑦 = 𝑏 → ( 𝜑 ↔ [ 𝑦 / 𝑏 ] 𝜑 ) )
52 sbceq1a ⊢ ( 𝑎 = 𝑥 → ( [ 𝑦 / 𝑏 ] 𝜑 ↔ [ 𝑥 / 𝑎 ] [ 𝑦 / 𝑏 ] 𝜑 ) )
53 52 equcoms ⊢ ( 𝑥 = 𝑎 → ( [ 𝑦 / 𝑏 ] 𝜑 ↔ [ 𝑥 / 𝑎 ] [ 𝑦 / 𝑏 ] 𝜑 ) )
54 51 53 sylan9bbr ⊢ ( ( 𝑥 = 𝑎 ∧ 𝑦 = 𝑏 ) → ( 𝜑 ↔ [ 𝑥 / 𝑎 ] [ 𝑦 / 𝑏 ] 𝜑 ) )
55 dfich2 ⊢ ( [ 𝑎 ⇄ 𝑏 ] 𝜑 ↔ ∀ 𝑥 ∀ 𝑦 ( [ 𝑥 / 𝑎 ] [ 𝑦 / 𝑏 ] 𝜑 ↔ [ 𝑦 / 𝑎 ] [ 𝑥 / 𝑏 ] 𝜑 ) )
56 2sp ⊢ ( ∀ 𝑥 ∀ 𝑦 ( [ 𝑥 / 𝑎 ] [ 𝑦 / 𝑏 ] 𝜑 ↔ [ 𝑦 / 𝑎 ] [ 𝑥 / 𝑏 ] 𝜑 ) → ( [ 𝑥 / 𝑎 ] [ 𝑦 / 𝑏 ] 𝜑 ↔ [ 𝑦 / 𝑎 ] [ 𝑥 / 𝑏 ] 𝜑 ) )
57 sbsbc ⊢ ( [ 𝑦 / 𝑏 ] 𝜑 ↔ [ 𝑦 / 𝑏 ] 𝜑 )
58 57 sbbii ⊢ ( [ 𝑥 / 𝑎 ] [ 𝑦 / 𝑏 ] 𝜑 ↔ [ 𝑥 / 𝑎 ] [ 𝑦 / 𝑏 ] 𝜑 )
59 sbsbc ⊢ ( [ 𝑥 / 𝑎 ] [ 𝑦 / 𝑏 ] 𝜑 ↔ [ 𝑥 / 𝑎 ] [ 𝑦 / 𝑏 ] 𝜑 )
60 58 59 bitri ⊢ ( [ 𝑥 / 𝑎 ] [ 𝑦 / 𝑏 ] 𝜑 ↔ [ 𝑥 / 𝑎 ] [ 𝑦 / 𝑏 ] 𝜑 )
61 sbsbc ⊢ ( [ 𝑥 / 𝑏 ] 𝜑 ↔ [ 𝑥 / 𝑏 ] 𝜑 )
62 61 sbbii ⊢ ( [ 𝑦 / 𝑎 ] [ 𝑥 / 𝑏 ] 𝜑 ↔ [ 𝑦 / 𝑎 ] [ 𝑥 / 𝑏 ] 𝜑 )
63 sbsbc ⊢ ( [ 𝑦 / 𝑎 ] [ 𝑥 / 𝑏 ] 𝜑 ↔ [ 𝑦 / 𝑎 ] [ 𝑥 / 𝑏 ] 𝜑 )
64 62 63 bitri ⊢ ( [ 𝑦 / 𝑎 ] [ 𝑥 / 𝑏 ] 𝜑 ↔ [ 𝑦 / 𝑎 ] [ 𝑥 / 𝑏 ] 𝜑 )
65 56 60 64 3bitr3g ⊢ ( ∀ 𝑥 ∀ 𝑦 ( [ 𝑥 / 𝑎 ] [ 𝑦 / 𝑏 ] 𝜑 ↔ [ 𝑦 / 𝑎 ] [ 𝑥 / 𝑏 ] 𝜑 ) → ( [ 𝑥 / 𝑎 ] [ 𝑦 / 𝑏 ] 𝜑 ↔ [ 𝑦 / 𝑎 ] [ 𝑥 / 𝑏 ] 𝜑 ) )
66 55 65 sylbi ⊢ ( [ 𝑎 ⇄ 𝑏 ] 𝜑 → ( [ 𝑥 / 𝑎 ] [ 𝑦 / 𝑏 ] 𝜑 ↔ [ 𝑦 / 𝑎 ] [ 𝑥 / 𝑏 ] 𝜑 ) )
67 66 biimpd ⊢ ( [ 𝑎 ⇄ 𝑏 ] 𝜑 → ( [ 𝑥 / 𝑎 ] [ 𝑦 / 𝑏 ] 𝜑 → [ 𝑦 / 𝑎 ] [ 𝑥 / 𝑏 ] 𝜑 ) )
68 67 adantr ⊢ ( ( [ 𝑎 ⇄ 𝑏 ] 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( [ 𝑥 / 𝑎 ] [ 𝑦 / 𝑏 ] 𝜑 → [ 𝑦 / 𝑎 ] [ 𝑥 / 𝑏 ] 𝜑 ) )
69 68 com12 ⊢ ( [ 𝑥 / 𝑎 ] [ 𝑦 / 𝑏 ] 𝜑 → ( ( [ 𝑎 ⇄ 𝑏 ] 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → [ 𝑦 / 𝑎 ] [ 𝑥 / 𝑏 ] 𝜑 ) )
70 54 69 syl6bi ⊢ ( ( 𝑥 = 𝑎 ∧ 𝑦 = 𝑏 ) → ( 𝜑 → ( ( [ 𝑎 ⇄ 𝑏 ] 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → [ 𝑦 / 𝑎 ] [ 𝑥 / 𝑏 ] 𝜑 ) ) )
71 49 70 sylbi ⊢ ( ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ → ( 𝜑 → ( ( [ 𝑎 ⇄ 𝑏 ] 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → [ 𝑦 / 𝑎 ] [ 𝑥 / 𝑏 ] 𝜑 ) ) )
72 71 imp ⊢ ( ( ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜑 ) → ( ( [ 𝑎 ⇄ 𝑏 ] 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → [ 𝑦 / 𝑎 ] [ 𝑥 / 𝑏 ] 𝜑 ) )
73 72 impcom ⊢ ( ( ( [ 𝑎 ⇄ 𝑏 ] 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ ( ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜑 ) ) → [ 𝑦 / 𝑎 ] [ 𝑥 / 𝑏 ] 𝜑 )
74 sbccom ⊢ ( [ 𝑥 / 𝑏 ] [ 𝑦 / 𝑎 ] 𝜑 ↔ [ 𝑦 / 𝑎 ] [ 𝑥 / 𝑏 ] 𝜑 )
75 73 74 sylibr ⊢ ( ( ( [ 𝑎 ⇄ 𝑏 ] 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ ( ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜑 ) ) → [ 𝑥 / 𝑏 ] [ 𝑦 / 𝑎 ] 𝜑 )
76 46 75 jca ⊢ ( ( ( [ 𝑎 ⇄ 𝑏 ] 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ ( ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜑 ) ) → ( ⟨ 𝑦 , 𝑥 ⟩ = ⟨ 𝑦 , 𝑥 ⟩ ∧ [ 𝑥 / 𝑏 ] [ 𝑦 / 𝑎 ] 𝜑 ) )
77 nfcv ⊢ Ⅎ 𝑏 𝑥
78 nfv ⊢ Ⅎ 𝑏 ⟨ 𝑦 , 𝑥 ⟩ = ⟨ 𝑦 , 𝑥 ⟩
79 nfsbc1v ⊢ Ⅎ 𝑏 [ 𝑥 / 𝑏 ] [ 𝑦 / 𝑎 ] 𝜑
80 78 79 nfan ⊢ Ⅎ 𝑏 ( ⟨ 𝑦 , 𝑥 ⟩ = ⟨ 𝑦 , 𝑥 ⟩ ∧ [ 𝑥 / 𝑏 ] [ 𝑦 / 𝑎 ] 𝜑 )
81 opeq2 ⊢ ( 𝑏 = 𝑥 → ⟨ 𝑦 , 𝑏 ⟩ = ⟨ 𝑦 , 𝑥 ⟩ )
82 81 eqeq2d ⊢ ( 𝑏 = 𝑥 → ( ⟨ 𝑦 , 𝑥 ⟩ = ⟨ 𝑦 , 𝑏 ⟩ ↔ ⟨ 𝑦 , 𝑥 ⟩ = ⟨ 𝑦 , 𝑥 ⟩ ) )
83 sbceq1a ⊢ ( 𝑏 = 𝑥 → ( [ 𝑦 / 𝑎 ] 𝜑 ↔ [ 𝑥 / 𝑏 ] [ 𝑦 / 𝑎 ] 𝜑 ) )
84 82 83 anbi12d ⊢ ( 𝑏 = 𝑥 → ( ( ⟨ 𝑦 , 𝑥 ⟩ = ⟨ 𝑦 , 𝑏 ⟩ ∧ [ 𝑦 / 𝑎 ] 𝜑 ) ↔ ( ⟨ 𝑦 , 𝑥 ⟩ = ⟨ 𝑦 , 𝑥 ⟩ ∧ [ 𝑥 / 𝑏 ] [ 𝑦 / 𝑎 ] 𝜑 ) ) )
85 77 80 84 spcegf ⊢ ( 𝑥 ∈ 𝑋 → ( ( ⟨ 𝑦 , 𝑥 ⟩ = ⟨ 𝑦 , 𝑥 ⟩ ∧ [ 𝑥 / 𝑏 ] [ 𝑦 / 𝑎 ] 𝜑 ) → ∃ 𝑏 ( ⟨ 𝑦 , 𝑥 ⟩ = ⟨ 𝑦 , 𝑏 ⟩ ∧ [ 𝑦 / 𝑎 ] 𝜑 ) ) )
86 45 76 85 sylc ⊢ ( ( ( [ 𝑎 ⇄ 𝑏 ] 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ ( ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜑 ) ) → ∃ 𝑏 ( ⟨ 𝑦 , 𝑥 ⟩ = ⟨ 𝑦 , 𝑏 ⟩ ∧ [ 𝑦 / 𝑎 ] 𝜑 ) )
87 nfcv ⊢ Ⅎ 𝑎 𝑦
88 nfv ⊢ Ⅎ 𝑎 ⟨ 𝑦 , 𝑥 ⟩ = ⟨ 𝑦 , 𝑏 ⟩
89 nfsbc1v ⊢ Ⅎ 𝑎 [ 𝑦 / 𝑎 ] 𝜑
90 88 89 nfan ⊢ Ⅎ 𝑎 ( ⟨ 𝑦 , 𝑥 ⟩ = ⟨ 𝑦 , 𝑏 ⟩ ∧ [ 𝑦 / 𝑎 ] 𝜑 )
91 90 nfex ⊢ Ⅎ 𝑎 ∃ 𝑏 ( ⟨ 𝑦 , 𝑥 ⟩ = ⟨ 𝑦 , 𝑏 ⟩ ∧ [ 𝑦 / 𝑎 ] 𝜑 )
92 opeq1 ⊢ ( 𝑎 = 𝑦 → ⟨ 𝑎 , 𝑏 ⟩ = ⟨ 𝑦 , 𝑏 ⟩ )
93 92 eqeq2d ⊢ ( 𝑎 = 𝑦 → ( ⟨ 𝑦 , 𝑥 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ↔ ⟨ 𝑦 , 𝑥 ⟩ = ⟨ 𝑦 , 𝑏 ⟩ ) )
94 sbceq1a ⊢ ( 𝑎 = 𝑦 → ( 𝜑 ↔ [ 𝑦 / 𝑎 ] 𝜑 ) )
95 93 94 anbi12d ⊢ ( 𝑎 = 𝑦 → ( ( ⟨ 𝑦 , 𝑥 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜑 ) ↔ ( ⟨ 𝑦 , 𝑥 ⟩ = ⟨ 𝑦 , 𝑏 ⟩ ∧ [ 𝑦 / 𝑎 ] 𝜑 ) ) )
96 95 exbidv ⊢ ( 𝑎 = 𝑦 → ( ∃ 𝑏 ( ⟨ 𝑦 , 𝑥 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜑 ) ↔ ∃ 𝑏 ( ⟨ 𝑦 , 𝑥 ⟩ = ⟨ 𝑦 , 𝑏 ⟩ ∧ [ 𝑦 / 𝑎 ] 𝜑 ) ) )
97 87 91 96 spcegf ⊢ ( 𝑦 ∈ 𝑋 → ( ∃ 𝑏 ( ⟨ 𝑦 , 𝑥 ⟩ = ⟨ 𝑦 , 𝑏 ⟩ ∧ [ 𝑦 / 𝑎 ] 𝜑 ) → ∃ 𝑎 ∃ 𝑏 ( ⟨ 𝑦 , 𝑥 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜑 ) ) )
98 42 86 97 sylc ⊢ ( ( ( [ 𝑎 ⇄ 𝑏 ] 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ ( ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜑 ) ) → ∃ 𝑎 ∃ 𝑏 ( ⟨ 𝑦 , 𝑥 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜑 ) )
99 simpl ⊢ ( ( 𝑦 = 𝑥 ∧ ( 𝑥 = 𝑎 ∧ 𝑦 = 𝑏 ) ) → 𝑦 = 𝑥 )
100 simprr ⊢ ( ( 𝑦 = 𝑥 ∧ ( 𝑥 = 𝑎 ∧ 𝑦 = 𝑏 ) ) → 𝑦 = 𝑏 )
101 simpl ⊢ ( ( 𝑥 = 𝑎 ∧ 𝑦 = 𝑏 ) → 𝑥 = 𝑎 )
102 101 adantl ⊢ ( ( 𝑦 = 𝑥 ∧ ( 𝑥 = 𝑎 ∧ 𝑦 = 𝑏 ) ) → 𝑥 = 𝑎 )
103 99 100 102 3eqtr3rd ⊢ ( ( 𝑦 = 𝑥 ∧ ( 𝑥 = 𝑎 ∧ 𝑦 = 𝑏 ) ) → 𝑎 = 𝑏 )
104 103 anim1i ⊢ ( ( ( 𝑦 = 𝑥 ∧ ( 𝑥 = 𝑎 ∧ 𝑦 = 𝑏 ) ) ∧ 𝜑 ) → ( 𝑎 = 𝑏 ∧ 𝜑 ) )
105 104 exp31 ⊢ ( 𝑦 = 𝑥 → ( ( 𝑥 = 𝑎 ∧ 𝑦 = 𝑏 ) → ( 𝜑 → ( 𝑎 = 𝑏 ∧ 𝜑 ) ) ) )
106 49 105 syl5bi ⊢ ( 𝑦 = 𝑥 → ( ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ → ( 𝜑 → ( 𝑎 = 𝑏 ∧ 𝜑 ) ) ) )
107 106 impd ⊢ ( 𝑦 = 𝑥 → ( ( ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜑 ) → ( 𝑎 = 𝑏 ∧ 𝜑 ) ) )
108 48 47 opth1 ⊢ ( ⟨ 𝑦 , 𝑥 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ → 𝑦 = 𝑥 )
109 107 108 syl11 ⊢ ( ( ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜑 ) → ( ⟨ 𝑦 , 𝑥 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝑎 = 𝑏 ∧ 𝜑 ) ) )
110 109 adantl ⊢ ( ( ( [ 𝑎 ⇄ 𝑏 ] 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ ( ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜑 ) ) → ( ⟨ 𝑦 , 𝑥 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝑎 = 𝑏 ∧ 𝜑 ) ) )
111 110 imp ⊢ ( ( ( ( [ 𝑎 ⇄ 𝑏 ] 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ ( ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜑 ) ) ∧ ⟨ 𝑦 , 𝑥 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ) → ( 𝑎 = 𝑏 ∧ 𝜑 ) )
112 111 19.8ad ⊢ ( ( ( ( [ 𝑎 ⇄ 𝑏 ] 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ ( ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜑 ) ) ∧ ⟨ 𝑦 , 𝑥 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ) → ∃ 𝑏 ( 𝑎 = 𝑏 ∧ 𝜑 ) )
113 112 19.8ad ⊢ ( ( ( ( [ 𝑎 ⇄ 𝑏 ] 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ ( ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜑 ) ) ∧ ⟨ 𝑦 , 𝑥 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ) → ∃ 𝑎 ∃ 𝑏 ( 𝑎 = 𝑏 ∧ 𝜑 ) )
114 113 ex ⊢ ( ( ( [ 𝑎 ⇄ 𝑏 ] 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ ( ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜑 ) ) → ( ⟨ 𝑦 , 𝑥 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ → ∃ 𝑎 ∃ 𝑏 ( 𝑎 = 𝑏 ∧ 𝜑 ) ) )
115 98 114 embantd ⊢ ( ( ( [ 𝑎 ⇄ 𝑏 ] 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ ( ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜑 ) ) → ( ( ∃ 𝑎 ∃ 𝑏 ( ⟨ 𝑦 , 𝑥 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜑 ) → ⟨ 𝑦 , 𝑥 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ) → ∃ 𝑎 ∃ 𝑏 ( 𝑎 = 𝑏 ∧ 𝜑 ) ) )
116 115 ex ⊢ ( ( [ 𝑎 ⇄ 𝑏 ] 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( ( ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜑 ) → ( ( ∃ 𝑎 ∃ 𝑏 ( ⟨ 𝑦 , 𝑥 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜑 ) → ⟨ 𝑦 , 𝑥 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ) → ∃ 𝑎 ∃ 𝑏 ( 𝑎 = 𝑏 ∧ 𝜑 ) ) ) )
117 40 116 syl5d ⊢ ( ( [ 𝑎 ⇄ 𝑏 ] 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( ( ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜑 ) → ( ∀ 𝑣 ∈ 𝑋 ∀ 𝑤 ∈ 𝑋 ( ∃ 𝑎 ∃ 𝑏 ( ⟨ 𝑣 , 𝑤 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜑 ) → ⟨ 𝑣 , 𝑤 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ) → ∃ 𝑎 ∃ 𝑏 ( 𝑎 = 𝑏 ∧ 𝜑 ) ) ) )
118 21 31 117 exlimd ⊢ ( ( [ 𝑎 ⇄ 𝑏 ] 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( ∃ 𝑏 ( ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜑 ) → ( ∀ 𝑣 ∈ 𝑋 ∀ 𝑤 ∈ 𝑋 ( ∃ 𝑎 ∃ 𝑏 ( ⟨ 𝑣 , 𝑤 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜑 ) → ⟨ 𝑣 , 𝑤 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ) → ∃ 𝑎 ∃ 𝑏 ( 𝑎 = 𝑏 ∧ 𝜑 ) ) ) )
119 10 18 118 exlimd ⊢ ( ( [ 𝑎 ⇄ 𝑏 ] 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( ∃ 𝑎 ∃ 𝑏 ( ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜑 ) → ( ∀ 𝑣 ∈ 𝑋 ∀ 𝑤 ∈ 𝑋 ( ∃ 𝑎 ∃ 𝑏 ( ⟨ 𝑣 , 𝑤 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜑 ) → ⟨ 𝑣 , 𝑤 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ) → ∃ 𝑎 ∃ 𝑏 ( 𝑎 = 𝑏 ∧ 𝜑 ) ) ) )
120 119 impd ⊢ ( ( [ 𝑎 ⇄ 𝑏 ] 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( ( ∃ 𝑎 ∃ 𝑏 ( ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜑 ) ∧ ∀ 𝑣 ∈ 𝑋 ∀ 𝑤 ∈ 𝑋 ( ∃ 𝑎 ∃ 𝑏 ( ⟨ 𝑣 , 𝑤 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜑 ) → ⟨ 𝑣 , 𝑤 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ) ) → ∃ 𝑎 ∃ 𝑏 ( 𝑎 = 𝑏 ∧ 𝜑 ) ) )
121 120 rexlimdvva ⊢ ( [ 𝑎 ⇄ 𝑏 ] 𝜑 → ( ∃ 𝑥 ∈ 𝑋 ∃ 𝑦 ∈ 𝑋 ( ∃ 𝑎 ∃ 𝑏 ( ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜑 ) ∧ ∀ 𝑣 ∈ 𝑋 ∀ 𝑤 ∈ 𝑋 ( ∃ 𝑎 ∃ 𝑏 ( ⟨ 𝑣 , 𝑤 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜑 ) → ⟨ 𝑣 , 𝑤 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ) ) → ∃ 𝑎 ∃ 𝑏 ( 𝑎 = 𝑏 ∧ 𝜑 ) ) )
122 7 121 syl5bi ⊢ ( [ 𝑎 ⇄ 𝑏 ] 𝜑 → ( ∃! 𝑝 ∈ ( 𝑋 × 𝑋 ) ∃ 𝑎 ∃ 𝑏 ( 𝑝 = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜑 ) → ∃ 𝑎 ∃ 𝑏 ( 𝑎 = 𝑏 ∧ 𝜑 ) ) )