Metamath Proof Explorer

Theorem ich2exprop

Description: If the setvar variables are interchangeable in a wff, there is an ordered pair fulfilling the wff iff there is an unordered pair fulfilling the wff. (Contributed by AV, 16-Jul-2023)

Ref Expression
Assertion ich2exprop ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ [ 𝑎 ⇄ 𝑏 ] 𝜑 ) → ( ∃ 𝑎 ∃ 𝑏 ( { 𝐴 , 𝐵 } = { 𝑎 , 𝑏 } ∧ 𝜑 ) ↔ ∃ 𝑎 ∃ 𝑏 ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜑 ) ) )

Proof

Step Hyp Ref Expression
1 nfv ⊢ Ⅎ 𝑎 𝐴 ∈ 𝑋
2 nfv ⊢ Ⅎ 𝑎 𝐵 ∈ 𝑋
3 nfich1 ⊢ Ⅎ 𝑎 [ 𝑎 ⇄ 𝑏 ] 𝜑
4 1 2 3 nf3an ⊢ Ⅎ 𝑎 ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ [ 𝑎 ⇄ 𝑏 ] 𝜑 )
5 nfv ⊢ Ⅎ 𝑎 ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑥 , 𝑦 ⟩
6 nfcv ⊢ Ⅎ 𝑎 𝑦
7 nfsbc1v ⊢ Ⅎ 𝑎 [ 𝑥 / 𝑎 ] 𝜑
8 6 7 nfsbcw ⊢ Ⅎ 𝑎 [ 𝑦 / 𝑏 ] [ 𝑥 / 𝑎 ] 𝜑
9 5 8 nfan ⊢ Ⅎ 𝑎 ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ∧ [ 𝑦 / 𝑏 ] [ 𝑥 / 𝑎 ] 𝜑 )
10 9 nfex ⊢ Ⅎ 𝑎 ∃ 𝑦 ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ∧ [ 𝑦 / 𝑏 ] [ 𝑥 / 𝑎 ] 𝜑 )
11 10 nfex ⊢ Ⅎ 𝑎 ∃ 𝑥 ∃ 𝑦 ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ∧ [ 𝑦 / 𝑏 ] [ 𝑥 / 𝑎 ] 𝜑 )
12 nfv ⊢ Ⅎ 𝑏 𝐴 ∈ 𝑋
13 nfv ⊢ Ⅎ 𝑏 𝐵 ∈ 𝑋
14 nfich2 ⊢ Ⅎ 𝑏 [ 𝑎 ⇄ 𝑏 ] 𝜑
15 12 13 14 nf3an ⊢ Ⅎ 𝑏 ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ [ 𝑎 ⇄ 𝑏 ] 𝜑 )
16 nfv ⊢ Ⅎ 𝑏 ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑥 , 𝑦 ⟩
17 nfsbc1v ⊢ Ⅎ 𝑏 [ 𝑦 / 𝑏 ] [ 𝑥 / 𝑎 ] 𝜑
18 16 17 nfan ⊢ Ⅎ 𝑏 ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ∧ [ 𝑦 / 𝑏 ] [ 𝑥 / 𝑎 ] 𝜑 )
19 18 nfex ⊢ Ⅎ 𝑏 ∃ 𝑦 ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ∧ [ 𝑦 / 𝑏 ] [ 𝑥 / 𝑎 ] 𝜑 )
20 19 nfex ⊢ Ⅎ 𝑏 ∃ 𝑥 ∃ 𝑦 ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ∧ [ 𝑦 / 𝑏 ] [ 𝑥 / 𝑎 ] 𝜑 )
21 vex ⊢ 𝑎 ∈ V
22 vex ⊢ 𝑏 ∈ V
23 preq12bg ⊢ ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ ( 𝑎 ∈ V ∧ 𝑏 ∈ V ) ) → ( { 𝐴 , 𝐵 } = { 𝑎 , 𝑏 } ↔ ( ( 𝐴 = 𝑎 ∧ 𝐵 = 𝑏 ) ∨ ( 𝐴 = 𝑏 ∧ 𝐵 = 𝑎 ) ) ) )
24 21 22 23 mpanr12 ⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( { 𝐴 , 𝐵 } = { 𝑎 , 𝑏 } ↔ ( ( 𝐴 = 𝑎 ∧ 𝐵 = 𝑏 ) ∨ ( 𝐴 = 𝑏 ∧ 𝐵 = 𝑎 ) ) ) )
25 24 3adant3 ⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ [ 𝑎 ⇄ 𝑏 ] 𝜑 ) → ( { 𝐴 , 𝐵 } = { 𝑎 , 𝑏 } ↔ ( ( 𝐴 = 𝑎 ∧ 𝐵 = 𝑏 ) ∨ ( 𝐴 = 𝑏 ∧ 𝐵 = 𝑎 ) ) ) )
26 or2expropbilem1 ⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( 𝐴 = 𝑎 ∧ 𝐵 = 𝑏 ) → ( 𝜑 → ∃ 𝑥 ∃ 𝑦 ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ∧ [ 𝑦 / 𝑏 ] [ 𝑥 / 𝑎 ] 𝜑 ) ) ) )
27 26 3adant3 ⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ [ 𝑎 ⇄ 𝑏 ] 𝜑 ) → ( ( 𝐴 = 𝑎 ∧ 𝐵 = 𝑏 ) → ( 𝜑 → ∃ 𝑥 ∃ 𝑦 ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ∧ [ 𝑦 / 𝑏 ] [ 𝑥 / 𝑎 ] 𝜑 ) ) ) )
28 ichcom ⊢ ( [ 𝑎 ⇄ 𝑏 ] 𝜑 ↔ [ 𝑏 ⇄ 𝑎 ] 𝜑 )
29 28 biimpi ⊢ ( [ 𝑎 ⇄ 𝑏 ] 𝜑 → [ 𝑏 ⇄ 𝑎 ] 𝜑 )
30 29 3ad2ant3 ⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ [ 𝑎 ⇄ 𝑏 ] 𝜑 ) → [ 𝑏 ⇄ 𝑎 ] 𝜑 )
31 30 adantr ⊢ ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ [ 𝑎 ⇄ 𝑏 ] 𝜑 ) ∧ 𝜑 ) → [ 𝑏 ⇄ 𝑎 ] 𝜑 )
32 22 21 pm3.2i ⊢ ( 𝑏 ∈ V ∧ 𝑎 ∈ V )
33 32 a1i ⊢ ( ( 𝐴 = 𝑏 ∧ 𝐵 = 𝑎 ) → ( 𝑏 ∈ V ∧ 𝑎 ∈ V ) )
34 31 33 anim12i ⊢ ( ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ [ 𝑎 ⇄ 𝑏 ] 𝜑 ) ∧ 𝜑 ) ∧ ( 𝐴 = 𝑏 ∧ 𝐵 = 𝑎 ) ) → ( [ 𝑏 ⇄ 𝑎 ] 𝜑 ∧ ( 𝑏 ∈ V ∧ 𝑎 ∈ V ) ) )
35 simpr ⊢ ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ [ 𝑎 ⇄ 𝑏 ] 𝜑 ) ∧ 𝜑 ) → 𝜑 )
36 opeq12 ⊢ ( ( 𝐴 = 𝑏 ∧ 𝐵 = 𝑎 ) → ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑏 , 𝑎 ⟩ )
37 35 36 anim12ci ⊢ ( ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ [ 𝑎 ⇄ 𝑏 ] 𝜑 ) ∧ 𝜑 ) ∧ ( 𝐴 = 𝑏 ∧ 𝐵 = 𝑎 ) ) → ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑏 , 𝑎 ⟩ ∧ 𝜑 ) )
38 nfv ⊢ Ⅎ 𝑥 ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑏 , 𝑎 ⟩ ∧ 𝜑 )
39 nfv ⊢ Ⅎ 𝑦 ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑏 , 𝑎 ⟩ ∧ 𝜑 )
40 opeq12 ⊢ ( ( 𝑥 = 𝑏 ∧ 𝑦 = 𝑎 ) → ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑏 , 𝑎 ⟩ )
41 40 eqeq2d ⊢ ( ( 𝑥 = 𝑏 ∧ 𝑦 = 𝑎 ) → ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ↔ ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑏 , 𝑎 ⟩ ) )
42 41 adantl ⊢ ( ( [ 𝑏 ⇄ 𝑎 ] 𝜑 ∧ ( 𝑥 = 𝑏 ∧ 𝑦 = 𝑎 ) ) → ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ↔ ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑏 , 𝑎 ⟩ ) )
43 dfsbcq ⊢ ( 𝑦 = 𝑎 → ( [ 𝑦 / 𝑏 ] [ 𝑥 / 𝑎 ] 𝜑 ↔ [ 𝑎 / 𝑏 ] [ 𝑥 / 𝑎 ] 𝜑 ) )
44 43 adantl ⊢ ( ( 𝑥 = 𝑏 ∧ 𝑦 = 𝑎 ) → ( [ 𝑦 / 𝑏 ] [ 𝑥 / 𝑎 ] 𝜑 ↔ [ 𝑎 / 𝑏 ] [ 𝑥 / 𝑎 ] 𝜑 ) )
45 44 adantl ⊢ ( ( [ 𝑏 ⇄ 𝑎 ] 𝜑 ∧ ( 𝑥 = 𝑏 ∧ 𝑦 = 𝑎 ) ) → ( [ 𝑦 / 𝑏 ] [ 𝑥 / 𝑎 ] 𝜑 ↔ [ 𝑎 / 𝑏 ] [ 𝑥 / 𝑎 ] 𝜑 ) )
46 sbceq1a ⊢ ( 𝑥 = 𝑏 → ( [ 𝑎 / 𝑏 ] [ 𝑥 / 𝑎 ] 𝜑 ↔ [ 𝑏 / 𝑥 ] [ 𝑎 / 𝑏 ] [ 𝑥 / 𝑎 ] 𝜑 ) )
47 46 adantr ⊢ ( ( 𝑥 = 𝑏 ∧ 𝑦 = 𝑎 ) → ( [ 𝑎 / 𝑏 ] [ 𝑥 / 𝑎 ] 𝜑 ↔ [ 𝑏 / 𝑥 ] [ 𝑎 / 𝑏 ] [ 𝑥 / 𝑎 ] 𝜑 ) )
48 df-ich ⊢ ( [ 𝑏 ⇄ 𝑎 ] 𝜑 ↔ ∀ 𝑏 ∀ 𝑎 ( [ 𝑏 / 𝑥 ] [ 𝑎 / 𝑏 ] [ 𝑥 / 𝑎 ] 𝜑 ↔ 𝜑 ) )
49 sbsbc ⊢ ( [ 𝑏 / 𝑥 ] [ 𝑎 / 𝑏 ] [ 𝑥 / 𝑎 ] 𝜑 ↔ [ 𝑏 / 𝑥 ] [ 𝑎 / 𝑏 ] [ 𝑥 / 𝑎 ] 𝜑 )
50 sbsbc ⊢ ( [ 𝑎 / 𝑏 ] [ 𝑥 / 𝑎 ] 𝜑 ↔ [ 𝑎 / 𝑏 ] [ 𝑥 / 𝑎 ] 𝜑 )
51 sbsbc ⊢ ( [ 𝑥 / 𝑎 ] 𝜑 ↔ [ 𝑥 / 𝑎 ] 𝜑 )
52 51 sbcbii ⊢ ( [ 𝑎 / 𝑏 ] [ 𝑥 / 𝑎 ] 𝜑 ↔ [ 𝑎 / 𝑏 ] [ 𝑥 / 𝑎 ] 𝜑 )
53 50 52 bitri ⊢ ( [ 𝑎 / 𝑏 ] [ 𝑥 / 𝑎 ] 𝜑 ↔ [ 𝑎 / 𝑏 ] [ 𝑥 / 𝑎 ] 𝜑 )
54 53 sbcbii ⊢ ( [ 𝑏 / 𝑥 ] [ 𝑎 / 𝑏 ] [ 𝑥 / 𝑎 ] 𝜑 ↔ [ 𝑏 / 𝑥 ] [ 𝑎 / 𝑏 ] [ 𝑥 / 𝑎 ] 𝜑 )
55 49 54 bitri ⊢ ( [ 𝑏 / 𝑥 ] [ 𝑎 / 𝑏 ] [ 𝑥 / 𝑎 ] 𝜑 ↔ [ 𝑏 / 𝑥 ] [ 𝑎 / 𝑏 ] [ 𝑥 / 𝑎 ] 𝜑 )
56 2sp ⊢ ( ∀ 𝑏 ∀ 𝑎 ( [ 𝑏 / 𝑥 ] [ 𝑎 / 𝑏 ] [ 𝑥 / 𝑎 ] 𝜑 ↔ 𝜑 ) → ( [ 𝑏 / 𝑥 ] [ 𝑎 / 𝑏 ] [ 𝑥 / 𝑎 ] 𝜑 ↔ 𝜑 ) )
57 55 56 bitr3id ⊢ ( ∀ 𝑏 ∀ 𝑎 ( [ 𝑏 / 𝑥 ] [ 𝑎 / 𝑏 ] [ 𝑥 / 𝑎 ] 𝜑 ↔ 𝜑 ) → ( [ 𝑏 / 𝑥 ] [ 𝑎 / 𝑏 ] [ 𝑥 / 𝑎 ] 𝜑 ↔ 𝜑 ) )
58 48 57 sylbi ⊢ ( [ 𝑏 ⇄ 𝑎 ] 𝜑 → ( [ 𝑏 / 𝑥 ] [ 𝑎 / 𝑏 ] [ 𝑥 / 𝑎 ] 𝜑 ↔ 𝜑 ) )
59 47 58 sylan9bbr ⊢ ( ( [ 𝑏 ⇄ 𝑎 ] 𝜑 ∧ ( 𝑥 = 𝑏 ∧ 𝑦 = 𝑎 ) ) → ( [ 𝑎 / 𝑏 ] [ 𝑥 / 𝑎 ] 𝜑 ↔ 𝜑 ) )
60 45 59 bitrd ⊢ ( ( [ 𝑏 ⇄ 𝑎 ] 𝜑 ∧ ( 𝑥 = 𝑏 ∧ 𝑦 = 𝑎 ) ) → ( [ 𝑦 / 𝑏 ] [ 𝑥 / 𝑎 ] 𝜑 ↔ 𝜑 ) )
61 42 60 anbi12d ⊢ ( ( [ 𝑏 ⇄ 𝑎 ] 𝜑 ∧ ( 𝑥 = 𝑏 ∧ 𝑦 = 𝑎 ) ) → ( ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ∧ [ 𝑦 / 𝑏 ] [ 𝑥 / 𝑎 ] 𝜑 ) ↔ ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑏 , 𝑎 ⟩ ∧ 𝜑 ) ) )
62 38 39 61 spc2ed ⊢ ( ( [ 𝑏 ⇄ 𝑎 ] 𝜑 ∧ ( 𝑏 ∈ V ∧ 𝑎 ∈ V ) ) → ( ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑏 , 𝑎 ⟩ ∧ 𝜑 ) → ∃ 𝑥 ∃ 𝑦 ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ∧ [ 𝑦 / 𝑏 ] [ 𝑥 / 𝑎 ] 𝜑 ) ) )
63 34 37 62 sylc ⊢ ( ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ [ 𝑎 ⇄ 𝑏 ] 𝜑 ) ∧ 𝜑 ) ∧ ( 𝐴 = 𝑏 ∧ 𝐵 = 𝑎 ) ) → ∃ 𝑥 ∃ 𝑦 ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ∧ [ 𝑦 / 𝑏 ] [ 𝑥 / 𝑎 ] 𝜑 ) )
64 63 exp31 ⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ [ 𝑎 ⇄ 𝑏 ] 𝜑 ) → ( 𝜑 → ( ( 𝐴 = 𝑏 ∧ 𝐵 = 𝑎 ) → ∃ 𝑥 ∃ 𝑦 ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ∧ [ 𝑦 / 𝑏 ] [ 𝑥 / 𝑎 ] 𝜑 ) ) ) )
65 64 com23 ⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ [ 𝑎 ⇄ 𝑏 ] 𝜑 ) → ( ( 𝐴 = 𝑏 ∧ 𝐵 = 𝑎 ) → ( 𝜑 → ∃ 𝑥 ∃ 𝑦 ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ∧ [ 𝑦 / 𝑏 ] [ 𝑥 / 𝑎 ] 𝜑 ) ) ) )
66 27 65 jaod ⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ [ 𝑎 ⇄ 𝑏 ] 𝜑 ) → ( ( ( 𝐴 = 𝑎 ∧ 𝐵 = 𝑏 ) ∨ ( 𝐴 = 𝑏 ∧ 𝐵 = 𝑎 ) ) → ( 𝜑 → ∃ 𝑥 ∃ 𝑦 ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ∧ [ 𝑦 / 𝑏 ] [ 𝑥 / 𝑎 ] 𝜑 ) ) ) )
67 25 66 sylbid ⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ [ 𝑎 ⇄ 𝑏 ] 𝜑 ) → ( { 𝐴 , 𝐵 } = { 𝑎 , 𝑏 } → ( 𝜑 → ∃ 𝑥 ∃ 𝑦 ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ∧ [ 𝑦 / 𝑏 ] [ 𝑥 / 𝑎 ] 𝜑 ) ) ) )
68 67 impd ⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ [ 𝑎 ⇄ 𝑏 ] 𝜑 ) → ( ( { 𝐴 , 𝐵 } = { 𝑎 , 𝑏 } ∧ 𝜑 ) → ∃ 𝑥 ∃ 𝑦 ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ∧ [ 𝑦 / 𝑏 ] [ 𝑥 / 𝑎 ] 𝜑 ) ) )
69 15 20 68 exlimd ⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ [ 𝑎 ⇄ 𝑏 ] 𝜑 ) → ( ∃ 𝑏 ( { 𝐴 , 𝐵 } = { 𝑎 , 𝑏 } ∧ 𝜑 ) → ∃ 𝑥 ∃ 𝑦 ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ∧ [ 𝑦 / 𝑏 ] [ 𝑥 / 𝑎 ] 𝜑 ) ) )
70 4 11 69 exlimd ⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ [ 𝑎 ⇄ 𝑏 ] 𝜑 ) → ( ∃ 𝑎 ∃ 𝑏 ( { 𝐴 , 𝐵 } = { 𝑎 , 𝑏 } ∧ 𝜑 ) → ∃ 𝑥 ∃ 𝑦 ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ∧ [ 𝑦 / 𝑏 ] [ 𝑥 / 𝑎 ] 𝜑 ) ) )
71 or2expropbilem2 ⊢ ( ∃ 𝑎 ∃ 𝑏 ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜑 ) ↔ ∃ 𝑥 ∃ 𝑦 ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ∧ [ 𝑦 / 𝑏 ] [ 𝑥 / 𝑎 ] 𝜑 ) )
72 70 71 syl6ibr ⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ [ 𝑎 ⇄ 𝑏 ] 𝜑 ) → ( ∃ 𝑎 ∃ 𝑏 ( { 𝐴 , 𝐵 } = { 𝑎 , 𝑏 } ∧ 𝜑 ) → ∃ 𝑎 ∃ 𝑏 ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜑 ) ) )
73 oppr ⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ → { 𝐴 , 𝐵 } = { 𝑎 , 𝑏 } ) )
74 73 anim1d ⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜑 ) → ( { 𝐴 , 𝐵 } = { 𝑎 , 𝑏 } ∧ 𝜑 ) ) )
75 74 2eximdv ⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ∃ 𝑎 ∃ 𝑏 ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜑 ) → ∃ 𝑎 ∃ 𝑏 ( { 𝐴 , 𝐵 } = { 𝑎 , 𝑏 } ∧ 𝜑 ) ) )
76 75 3adant3 ⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ [ 𝑎 ⇄ 𝑏 ] 𝜑 ) → ( ∃ 𝑎 ∃ 𝑏 ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜑 ) → ∃ 𝑎 ∃ 𝑏 ( { 𝐴 , 𝐵 } = { 𝑎 , 𝑏 } ∧ 𝜑 ) ) )
77 72 76 impbid ⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ [ 𝑎 ⇄ 𝑏 ] 𝜑 ) → ( ∃ 𝑎 ∃ 𝑏 ( { 𝐴 , 𝐵 } = { 𝑎 , 𝑏 } ∧ 𝜑 ) ↔ ∃ 𝑎 ∃ 𝑏 ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜑 ) ) )