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
|
bitrid |
⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ∃! 𝑥 ∈ { 𝐴 , 𝐵 } 𝜑 ↔ ( ( 𝜓 ∧ ( 𝜒 → 𝐴 = 𝐵 ) ) ∨ ( 𝜒 ∧ ( 𝜓 → 𝐴 = 𝐵 ) ) ) ) ) |