Metamath Proof Explorer

Theorem reuprg0

Description: Convert a restricted existential uniqueness over a pair to a disjunction of conjunctions. (Contributed by AV, 2-Apr-2023)

Ref Expression
Hypotheses reuprg.1 ⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) )
reuprg.2 ⊢ ( 𝑥 = 𝐵 → ( 𝜑 ↔ 𝜒 ) )
Assertion reuprg0 ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ∃! 𝑥 ∈ { 𝐴 , 𝐵 } 𝜑 ↔ ( ( 𝜓 ∧ ( 𝜒 → 𝐴 = 𝐵 ) ) ∨ ( 𝜒 ∧ ( 𝜓 → 𝐴 = 𝐵 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 reuprg.1 ⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) )
2 reuprg.2 ⊢ ( 𝑥 = 𝐵 → ( 𝜑 ↔ 𝜒 ) )
3 nfsbc1v ⊢ Ⅎ 𝑥 [ 𝑐 / 𝑥 ] 𝜑
4 nfsbc1v ⊢ Ⅎ 𝑥 [ 𝑤 / 𝑥 ] 𝜑
5 sbceq1a ⊢ ( 𝑥 = 𝑤 → ( 𝜑 ↔ [ 𝑤 / 𝑥 ] 𝜑 ) )
6 dfsbcq ⊢ ( 𝑤 = 𝑐 → ( [ 𝑤 / 𝑥 ] 𝜑 ↔ [ 𝑐 / 𝑥 ] 𝜑 ) )
7 3 4 5 6 reu8nf ⊢ ( ∃! 𝑥 ∈ { 𝐴 , 𝐵 } 𝜑 ↔ ∃ 𝑥 ∈ { 𝐴 , 𝐵 } ( 𝜑 ∧ ∀ 𝑐 ∈ { 𝐴 , 𝐵 } ( [ 𝑐 / 𝑥 ] 𝜑 → 𝑥 = 𝑐 ) ) )
8 nfv ⊢ Ⅎ 𝑥 𝜓
9 nfcv ⊢ Ⅎ 𝑥 { 𝐴 , 𝐵 }
10 nfv ⊢ Ⅎ 𝑥 𝐴 = 𝑐
11 3 10 nfim ⊢ Ⅎ 𝑥 ( [ 𝑐 / 𝑥 ] 𝜑 → 𝐴 = 𝑐 )
12 9 11 nfralw ⊢ Ⅎ 𝑥 ∀ 𝑐 ∈ { 𝐴 , 𝐵 } ( [ 𝑐 / 𝑥 ] 𝜑 → 𝐴 = 𝑐 )
13 8 12 nfan ⊢ Ⅎ 𝑥 ( 𝜓 ∧ ∀ 𝑐 ∈ { 𝐴 , 𝐵 } ( [ 𝑐 / 𝑥 ] 𝜑 → 𝐴 = 𝑐 ) )
14 nfv ⊢ Ⅎ 𝑥 𝜒
15 nfv ⊢ Ⅎ 𝑥 𝐵 = 𝑐
16 3 15 nfim ⊢ Ⅎ 𝑥 ( [ 𝑐 / 𝑥 ] 𝜑 → 𝐵 = 𝑐 )
17 9 16 nfralw ⊢ Ⅎ 𝑥 ∀ 𝑐 ∈ { 𝐴 , 𝐵 } ( [ 𝑐 / 𝑥 ] 𝜑 → 𝐵 = 𝑐 )
18 14 17 nfan ⊢ Ⅎ 𝑥 ( 𝜒 ∧ ∀ 𝑐 ∈ { 𝐴 , 𝐵 } ( [ 𝑐 / 𝑥 ] 𝜑 → 𝐵 = 𝑐 ) )
19 eqeq1 ⊢ ( 𝑥 = 𝐴 → ( 𝑥 = 𝑐 ↔ 𝐴 = 𝑐 ) )
20 19 imbi2d ⊢ ( 𝑥 = 𝐴 → ( ( [ 𝑐 / 𝑥 ] 𝜑 → 𝑥 = 𝑐 ) ↔ ( [ 𝑐 / 𝑥 ] 𝜑 → 𝐴 = 𝑐 ) ) )
21 20 ralbidv ⊢ ( 𝑥 = 𝐴 → ( ∀ 𝑐 ∈ { 𝐴 , 𝐵 } ( [ 𝑐 / 𝑥 ] 𝜑 → 𝑥 = 𝑐 ) ↔ ∀ 𝑐 ∈ { 𝐴 , 𝐵 } ( [ 𝑐 / 𝑥 ] 𝜑 → 𝐴 = 𝑐 ) ) )
22 1 21 anbi12d ⊢ ( 𝑥 = 𝐴 → ( ( 𝜑 ∧ ∀ 𝑐 ∈ { 𝐴 , 𝐵 } ( [ 𝑐 / 𝑥 ] 𝜑 → 𝑥 = 𝑐 ) ) ↔ ( 𝜓 ∧ ∀ 𝑐 ∈ { 𝐴 , 𝐵 } ( [ 𝑐 / 𝑥 ] 𝜑 → 𝐴 = 𝑐 ) ) ) )
23 eqeq1 ⊢ ( 𝑥 = 𝐵 → ( 𝑥 = 𝑐 ↔ 𝐵 = 𝑐 ) )
24 23 imbi2d ⊢ ( 𝑥 = 𝐵 → ( ( [ 𝑐 / 𝑥 ] 𝜑 → 𝑥 = 𝑐 ) ↔ ( [ 𝑐 / 𝑥 ] 𝜑 → 𝐵 = 𝑐 ) ) )
25 24 ralbidv ⊢ ( 𝑥 = 𝐵 → ( ∀ 𝑐 ∈ { 𝐴 , 𝐵 } ( [ 𝑐 / 𝑥 ] 𝜑 → 𝑥 = 𝑐 ) ↔ ∀ 𝑐 ∈ { 𝐴 , 𝐵 } ( [ 𝑐 / 𝑥 ] 𝜑 → 𝐵 = 𝑐 ) ) )
26 2 25 anbi12d ⊢ ( 𝑥 = 𝐵 → ( ( 𝜑 ∧ ∀ 𝑐 ∈ { 𝐴 , 𝐵 } ( [ 𝑐 / 𝑥 ] 𝜑 → 𝑥 = 𝑐 ) ) ↔ ( 𝜒 ∧ ∀ 𝑐 ∈ { 𝐴 , 𝐵 } ( [ 𝑐 / 𝑥 ] 𝜑 → 𝐵 = 𝑐 ) ) ) )
27 13 18 22 26 rexprgf ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ∃ 𝑥 ∈ { 𝐴 , 𝐵 } ( 𝜑 ∧ ∀ 𝑐 ∈ { 𝐴 , 𝐵 } ( [ 𝑐 / 𝑥 ] 𝜑 → 𝑥 = 𝑐 ) ) ↔ ( ( 𝜓 ∧ ∀ 𝑐 ∈ { 𝐴 , 𝐵 } ( [ 𝑐 / 𝑥 ] 𝜑 → 𝐴 = 𝑐 ) ) ∨ ( 𝜒 ∧ ∀ 𝑐 ∈ { 𝐴 , 𝐵 } ( [ 𝑐 / 𝑥 ] 𝜑 → 𝐵 = 𝑐 ) ) ) ) )
28 dfsbcq ⊢ ( 𝑐 = 𝐴 → ( [ 𝑐 / 𝑥 ] 𝜑 ↔ [ 𝐴 / 𝑥 ] 𝜑 ) )
29 eqeq2 ⊢ ( 𝑐 = 𝐴 → ( 𝐴 = 𝑐 ↔ 𝐴 = 𝐴 ) )
30 28 29 imbi12d ⊢ ( 𝑐 = 𝐴 → ( ( [ 𝑐 / 𝑥 ] 𝜑 → 𝐴 = 𝑐 ) ↔ ( [ 𝐴 / 𝑥 ] 𝜑 → 𝐴 = 𝐴 ) ) )
31 dfsbcq ⊢ ( 𝑐 = 𝐵 → ( [ 𝑐 / 𝑥 ] 𝜑 ↔ [ 𝐵 / 𝑥 ] 𝜑 ) )
32 eqeq2 ⊢ ( 𝑐 = 𝐵 → ( 𝐴 = 𝑐 ↔ 𝐴 = 𝐵 ) )
33 31 32 imbi12d ⊢ ( 𝑐 = 𝐵 → ( ( [ 𝑐 / 𝑥 ] 𝜑 → 𝐴 = 𝑐 ) ↔ ( [ 𝐵 / 𝑥 ] 𝜑 → 𝐴 = 𝐵 ) ) )
34 30 33 ralprg ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ∀ 𝑐 ∈ { 𝐴 , 𝐵 } ( [ 𝑐 / 𝑥 ] 𝜑 → 𝐴 = 𝑐 ) ↔ ( ( [ 𝐴 / 𝑥 ] 𝜑 → 𝐴 = 𝐴 ) ∧ ( [ 𝐵 / 𝑥 ] 𝜑 → 𝐴 = 𝐵 ) ) ) )
35 eqidd ⊢ ( [ 𝐴 / 𝑥 ] 𝜑 → 𝐴 = 𝐴 )
36 35 biantrur ⊢ ( ( [ 𝐵 / 𝑥 ] 𝜑 → 𝐴 = 𝐵 ) ↔ ( ( [ 𝐴 / 𝑥 ] 𝜑 → 𝐴 = 𝐴 ) ∧ ( [ 𝐵 / 𝑥 ] 𝜑 → 𝐴 = 𝐵 ) ) )
37 2 sbcieg ⊢ ( 𝐵 ∈ 𝑊 → ( [ 𝐵 / 𝑥 ] 𝜑 ↔ 𝜒 ) )
38 37 adantl ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( [ 𝐵 / 𝑥 ] 𝜑 ↔ 𝜒 ) )
39 38 imbi1d ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ( [ 𝐵 / 𝑥 ] 𝜑 → 𝐴 = 𝐵 ) ↔ ( 𝜒 → 𝐴 = 𝐵 ) ) )
40 36 39 bitr3id ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ( ( [ 𝐴 / 𝑥 ] 𝜑 → 𝐴 = 𝐴 ) ∧ ( [ 𝐵 / 𝑥 ] 𝜑 → 𝐴 = 𝐵 ) ) ↔ ( 𝜒 → 𝐴 = 𝐵 ) ) )
41 34 40 bitrd ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ∀ 𝑐 ∈ { 𝐴 , 𝐵 } ( [ 𝑐 / 𝑥 ] 𝜑 → 𝐴 = 𝑐 ) ↔ ( 𝜒 → 𝐴 = 𝐵 ) ) )
42 41 anbi2d ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ( 𝜓 ∧ ∀ 𝑐 ∈ { 𝐴 , 𝐵 } ( [ 𝑐 / 𝑥 ] 𝜑 → 𝐴 = 𝑐 ) ) ↔ ( 𝜓 ∧ ( 𝜒 → 𝐴 = 𝐵 ) ) ) )
43 eqeq2 ⊢ ( 𝑐 = 𝐴 → ( 𝐵 = 𝑐 ↔ 𝐵 = 𝐴 ) )
44 28 43 imbi12d ⊢ ( 𝑐 = 𝐴 → ( ( [ 𝑐 / 𝑥 ] 𝜑 → 𝐵 = 𝑐 ) ↔ ( [ 𝐴 / 𝑥 ] 𝜑 → 𝐵 = 𝐴 ) ) )
45 eqeq2 ⊢ ( 𝑐 = 𝐵 → ( 𝐵 = 𝑐 ↔ 𝐵 = 𝐵 ) )
46 31 45 imbi12d ⊢ ( 𝑐 = 𝐵 → ( ( [ 𝑐 / 𝑥 ] 𝜑 → 𝐵 = 𝑐 ) ↔ ( [ 𝐵 / 𝑥 ] 𝜑 → 𝐵 = 𝐵 ) ) )
47 44 46 ralprg ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ∀ 𝑐 ∈ { 𝐴 , 𝐵 } ( [ 𝑐 / 𝑥 ] 𝜑 → 𝐵 = 𝑐 ) ↔ ( ( [ 𝐴 / 𝑥 ] 𝜑 → 𝐵 = 𝐴 ) ∧ ( [ 𝐵 / 𝑥 ] 𝜑 → 𝐵 = 𝐵 ) ) ) )
48 eqidd ⊢ ( [ 𝐵 / 𝑥 ] 𝜑 → 𝐵 = 𝐵 )
49 48 biantru ⊢ ( ( [ 𝐴 / 𝑥 ] 𝜑 → 𝐵 = 𝐴 ) ↔ ( ( [ 𝐴 / 𝑥 ] 𝜑 → 𝐵 = 𝐴 ) ∧ ( [ 𝐵 / 𝑥 ] 𝜑 → 𝐵 = 𝐵 ) ) )
50 1 sbcieg ⊢ ( 𝐴 ∈ 𝑉 → ( [ 𝐴 / 𝑥 ] 𝜑 ↔ 𝜓 ) )
51 50 adantr ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( [ 𝐴 / 𝑥 ] 𝜑 ↔ 𝜓 ) )
52 51 imbi1d ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ( [ 𝐴 / 𝑥 ] 𝜑 → 𝐵 = 𝐴 ) ↔ ( 𝜓 → 𝐵 = 𝐴 ) ) )
53 49 52 bitr3id ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ( ( [ 𝐴 / 𝑥 ] 𝜑 → 𝐵 = 𝐴 ) ∧ ( [ 𝐵 / 𝑥 ] 𝜑 → 𝐵 = 𝐵 ) ) ↔ ( 𝜓 → 𝐵 = 𝐴 ) ) )
54 47 53 bitrd ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ∀ 𝑐 ∈ { 𝐴 , 𝐵 } ( [ 𝑐 / 𝑥 ] 𝜑 → 𝐵 = 𝑐 ) ↔ ( 𝜓 → 𝐵 = 𝐴 ) ) )
55 54 anbi2d ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ( 𝜒 ∧ ∀ 𝑐 ∈ { 𝐴 , 𝐵 } ( [ 𝑐 / 𝑥 ] 𝜑 → 𝐵 = 𝑐 ) ) ↔ ( 𝜒 ∧ ( 𝜓 → 𝐵 = 𝐴 ) ) ) )
56 eqcom ⊢ ( 𝐵 = 𝐴 ↔ 𝐴 = 𝐵 )
57 56 imbi2i ⊢ ( ( 𝜓 → 𝐵 = 𝐴 ) ↔ ( 𝜓 → 𝐴 = 𝐵 ) )
58 57 anbi2i ⊢ ( ( 𝜒 ∧ ( 𝜓 → 𝐵 = 𝐴 ) ) ↔ ( 𝜒 ∧ ( 𝜓 → 𝐴 = 𝐵 ) ) )
59 55 58 bitrdi ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ( 𝜒 ∧ ∀ 𝑐 ∈ { 𝐴 , 𝐵 } ( [ 𝑐 / 𝑥 ] 𝜑 → 𝐵 = 𝑐 ) ) ↔ ( 𝜒 ∧ ( 𝜓 → 𝐴 = 𝐵 ) ) ) )
60 42 59 orbi12d ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ( ( 𝜓 ∧ ∀ 𝑐 ∈ { 𝐴 , 𝐵 } ( [ 𝑐 / 𝑥 ] 𝜑 → 𝐴 = 𝑐 ) ) ∨ ( 𝜒 ∧ ∀ 𝑐 ∈ { 𝐴 , 𝐵 } ( [ 𝑐 / 𝑥 ] 𝜑 → 𝐵 = 𝑐 ) ) ) ↔ ( ( 𝜓 ∧ ( 𝜒 → 𝐴 = 𝐵 ) ) ∨ ( 𝜒 ∧ ( 𝜓 → 𝐴 = 𝐵 ) ) ) ) )
61 27 60 bitrd ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ∃ 𝑥 ∈ { 𝐴 , 𝐵 } ( 𝜑 ∧ ∀ 𝑐 ∈ { 𝐴 , 𝐵 } ( [ 𝑐 / 𝑥 ] 𝜑 → 𝑥 = 𝑐 ) ) ↔ ( ( 𝜓 ∧ ( 𝜒 → 𝐴 = 𝐵 ) ) ∨ ( 𝜒 ∧ ( 𝜓 → 𝐴 = 𝐵 ) ) ) ) )
62 7 61 syl5bb ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ∃! 𝑥 ∈ { 𝐴 , 𝐵 } 𝜑 ↔ ( ( 𝜓 ∧ ( 𝜒 → 𝐴 = 𝐵 ) ) ∨ ( 𝜒 ∧ ( 𝜓 → 𝐴 = 𝐵 ) ) ) ) )