Proof of Theorem rexxfrd
Step | Hyp | Ref
| Expression |
1 | | nfv 1418 |
. . . . 5
⊢
Ⅎyψ |
2 | 1 | 19.3 1443 |
. . . 4
⊢ (∀yψ ↔ ψ) |
3 | | ralxfrd.2 |
. . . . 5
⊢ ((φ ∧ x ∈ B) → ∃y ∈ 𝐶 x =
A) |
4 | | df-rex 2306 |
. . . . . . . 8
⊢ (∃y ∈ 𝐶 x =
A ↔ ∃y(y ∈ 𝐶 ∧ x = A)) |
5 | | 19.29 1508 |
. . . . . . . . . 10
⊢ ((∀yψ ∧ ∃y(y ∈ 𝐶 ∧ x = A)) → ∃y(ψ ∧
(y ∈
𝐶 ∧ x = A))) |
6 | | an12 495 |
. . . . . . . . . . 11
⊢ ((ψ ∧
(y ∈
𝐶 ∧ x = A)) ↔ (y
∈ 𝐶 ∧ (ψ ∧ x = A))) |
7 | 6 | exbii 1493 |
. . . . . . . . . 10
⊢ (∃y(ψ ∧
(y ∈
𝐶 ∧ x = A)) ↔ ∃y(y ∈ 𝐶 ∧ (ψ ∧ x = A))) |
8 | 5, 7 | sylib 127 |
. . . . . . . . 9
⊢ ((∀yψ ∧ ∃y(y ∈ 𝐶 ∧ x = A)) → ∃y(y ∈ 𝐶 ∧ (ψ ∧ x = A))) |
9 | | df-rex 2306 |
. . . . . . . . 9
⊢ (∃y ∈ 𝐶 (ψ
∧ x =
A) ↔ ∃y(y ∈ 𝐶 ∧ (ψ ∧ x = A))) |
10 | 8, 9 | sylibr 137 |
. . . . . . . 8
⊢ ((∀yψ ∧ ∃y(y ∈ 𝐶 ∧ x = A)) → ∃y ∈ 𝐶 (ψ
∧ x =
A)) |
11 | 4, 10 | sylan2b 271 |
. . . . . . 7
⊢ ((∀yψ ∧ ∃y ∈ 𝐶 x =
A) → ∃y ∈ 𝐶 (ψ
∧ x =
A)) |
12 | | ralxfrd.3 |
. . . . . . . . . . 11
⊢ ((φ ∧ x = A) →
(ψ ↔ χ)) |
13 | 12 | biimpd 132 |
. . . . . . . . . 10
⊢ ((φ ∧ x = A) →
(ψ → χ)) |
14 | 13 | expimpd 345 |
. . . . . . . . 9
⊢ (φ → ((x = A ∧ ψ) →
χ)) |
15 | 14 | ancomsd 256 |
. . . . . . . 8
⊢ (φ → ((ψ ∧ x = A) →
χ)) |
16 | 15 | reximdv 2414 |
. . . . . . 7
⊢ (φ → (∃y ∈ 𝐶 (ψ
∧ x =
A) → ∃y ∈ 𝐶 χ)) |
17 | 11, 16 | syl5 28 |
. . . . . 6
⊢ (φ → ((∀yψ ∧ ∃y ∈ 𝐶 x =
A) → ∃y ∈ 𝐶 χ)) |
18 | 17 | adantr 261 |
. . . . 5
⊢ ((φ ∧ x ∈ B) → ((∀yψ ∧ ∃y ∈ 𝐶 x =
A) → ∃y ∈ 𝐶 χ)) |
19 | 3, 18 | mpan2d 404 |
. . . 4
⊢ ((φ ∧ x ∈ B) → (∀yψ → ∃y ∈ 𝐶 χ)) |
20 | 2, 19 | syl5bir 142 |
. . 3
⊢ ((φ ∧ x ∈ B) → (ψ
→ ∃y ∈ 𝐶 χ)) |
21 | 20 | rexlimdva 2427 |
. 2
⊢ (φ → (∃x ∈ B ψ → ∃y ∈ 𝐶 χ)) |
22 | | ralxfrd.1 |
. . . 4
⊢ ((φ ∧ y ∈ 𝐶) → A ∈ B) |
23 | 12 | adantlr 446 |
. . . 4
⊢ (((φ ∧ y ∈ 𝐶) ∧ x = A) → (ψ
↔ χ)) |
24 | 22, 23 | rspcedv 2654 |
. . 3
⊢ ((φ ∧ y ∈ 𝐶) → (χ → ∃x ∈ B ψ)) |
25 | 24 | rexlimdva 2427 |
. 2
⊢ (φ → (∃y ∈ 𝐶 χ
→ ∃x ∈ B ψ)) |
26 | 21, 25 | impbid 120 |
1
⊢ (φ → (∃x ∈ B ψ ↔ ∃y ∈ 𝐶 χ)) |