Proof of Theorem cbvrexdva2OLD
Step | Hyp | Ref
| Expression |
1 | | simpr 487 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → 𝑥 = 𝑦) |
2 | | cbvraldva2.2 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → 𝐴 = 𝐵) |
3 | 1, 2 | eleq12d 2907 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐵)) |
4 | | cbvraldva2.1 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒)) |
5 | 3, 4 | anbi12d 632 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → ((𝑥 ∈ 𝐴 ∧ 𝜓) ↔ (𝑦 ∈ 𝐵 ∧ 𝜒))) |
6 | 5 | notbid 320 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (¬ (𝑥 ∈ 𝐴 ∧ 𝜓) ↔ ¬ (𝑦 ∈ 𝐵 ∧ 𝜒))) |
7 | 6 | expcom 416 |
. . . . . . . 8
⊢ (𝑥 = 𝑦 → (𝜑 → (¬ (𝑥 ∈ 𝐴 ∧ 𝜓) ↔ ¬ (𝑦 ∈ 𝐵 ∧ 𝜒)))) |
8 | 7 | pm5.74d 275 |
. . . . . . 7
⊢ (𝑥 = 𝑦 → ((𝜑 → ¬ (𝑥 ∈ 𝐴 ∧ 𝜓)) ↔ (𝜑 → ¬ (𝑦 ∈ 𝐵 ∧ 𝜒)))) |
9 | 8 | cbvalvw 2043 |
. . . . . 6
⊢
(∀𝑥(𝜑 → ¬ (𝑥 ∈ 𝐴 ∧ 𝜓)) ↔ ∀𝑦(𝜑 → ¬ (𝑦 ∈ 𝐵 ∧ 𝜒))) |
10 | | 19.21v 1940 |
. . . . . 6
⊢
(∀𝑥(𝜑 → ¬ (𝑥 ∈ 𝐴 ∧ 𝜓)) ↔ (𝜑 → ∀𝑥 ¬ (𝑥 ∈ 𝐴 ∧ 𝜓))) |
11 | | 19.21v 1940 |
. . . . . 6
⊢
(∀𝑦(𝜑 → ¬ (𝑦 ∈ 𝐵 ∧ 𝜒)) ↔ (𝜑 → ∀𝑦 ¬ (𝑦 ∈ 𝐵 ∧ 𝜒))) |
12 | 9, 10, 11 | 3bitr3i 303 |
. . . . 5
⊢ ((𝜑 → ∀𝑥 ¬ (𝑥 ∈ 𝐴 ∧ 𝜓)) ↔ (𝜑 → ∀𝑦 ¬ (𝑦 ∈ 𝐵 ∧ 𝜒))) |
13 | 12 | pm5.74ri 274 |
. . . 4
⊢ (𝜑 → (∀𝑥 ¬ (𝑥 ∈ 𝐴 ∧ 𝜓) ↔ ∀𝑦 ¬ (𝑦 ∈ 𝐵 ∧ 𝜒))) |
14 | | alnex 1782 |
. . . 4
⊢
(∀𝑥 ¬
(𝑥 ∈ 𝐴 ∧ 𝜓) ↔ ¬ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜓)) |
15 | | alnex 1782 |
. . . 4
⊢
(∀𝑦 ¬
(𝑦 ∈ 𝐵 ∧ 𝜒) ↔ ¬ ∃𝑦(𝑦 ∈ 𝐵 ∧ 𝜒)) |
16 | 13, 14, 15 | 3bitr3g 315 |
. . 3
⊢ (𝜑 → (¬ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜓) ↔ ¬ ∃𝑦(𝑦 ∈ 𝐵 ∧ 𝜒))) |
17 | 16 | con4bid 319 |
. 2
⊢ (𝜑 → (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜓) ↔ ∃𝑦(𝑦 ∈ 𝐵 ∧ 𝜒))) |
18 | | df-rex 3144 |
. 2
⊢
(∃𝑥 ∈
𝐴 𝜓 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜓)) |
19 | | df-rex 3144 |
. 2
⊢
(∃𝑦 ∈
𝐵 𝜒 ↔ ∃𝑦(𝑦 ∈ 𝐵 ∧ 𝜒)) |
20 | 17, 18, 19 | 3bitr4g 316 |
1
⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑦 ∈ 𝐵 𝜒)) |