Metamath Proof Explorer

Theorem reupr

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

Ref Expression
Hypotheses reupr.a ⊢ ( 𝑝 = { 𝑎 , 𝑏 } → ( 𝜓 ↔ 𝜒 ) )
reupr.x ⊢ ( 𝑝 = { 𝑥 , 𝑦 } → ( 𝜓 ↔ 𝜃 ) )
Assertion reupr ( 𝑋 ∈ 𝑉 → ( ∃! 𝑝 ∈ ( Pairs ‘ 𝑋 ) 𝜓 ↔ ∃ 𝑎 ∈ 𝑋 ∃ 𝑏 ∈ 𝑋 ( 𝜒 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝜃 → { 𝑥 , 𝑦 } = { 𝑎 , 𝑏 } ) ) ) )

Proof

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