Proof of Theorem rexdifi
| Step | Hyp | Ref
| Expression |
| 1 | | df-rex 3071 |
. . 3
⊢
(∃𝑥 ∈
𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)) |
| 2 | | df-ral 3062 |
. . 3
⊢
(∀𝑥 ∈
𝐵 ¬ 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐵 → ¬ 𝜑)) |
| 3 | | nfa1 2151 |
. . . . 5
⊢
Ⅎ𝑥∀𝑥(𝑥 ∈ 𝐵 → ¬ 𝜑) |
| 4 | | simprl 771 |
. . . . . . . 8
⊢
((∀𝑥(𝑥 ∈ 𝐵 → ¬ 𝜑) ∧ (𝑥 ∈ 𝐴 ∧ 𝜑)) → 𝑥 ∈ 𝐴) |
| 5 | | con2 135 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ 𝐵 → ¬ 𝜑) → (𝜑 → ¬ 𝑥 ∈ 𝐵)) |
| 6 | 5 | sps 2185 |
. . . . . . . . . . 11
⊢
(∀𝑥(𝑥 ∈ 𝐵 → ¬ 𝜑) → (𝜑 → ¬ 𝑥 ∈ 𝐵)) |
| 7 | 6 | com12 32 |
. . . . . . . . . 10
⊢ (𝜑 → (∀𝑥(𝑥 ∈ 𝐵 → ¬ 𝜑) → ¬ 𝑥 ∈ 𝐵)) |
| 8 | 7 | adantl 481 |
. . . . . . . . 9
⊢ ((𝑥 ∈ 𝐴 ∧ 𝜑) → (∀𝑥(𝑥 ∈ 𝐵 → ¬ 𝜑) → ¬ 𝑥 ∈ 𝐵)) |
| 9 | 8 | impcom 407 |
. . . . . . . 8
⊢
((∀𝑥(𝑥 ∈ 𝐵 → ¬ 𝜑) ∧ (𝑥 ∈ 𝐴 ∧ 𝜑)) → ¬ 𝑥 ∈ 𝐵) |
| 10 | 4, 9 | eldifd 3962 |
. . . . . . 7
⊢
((∀𝑥(𝑥 ∈ 𝐵 → ¬ 𝜑) ∧ (𝑥 ∈ 𝐴 ∧ 𝜑)) → 𝑥 ∈ (𝐴 ∖ 𝐵)) |
| 11 | | simprr 773 |
. . . . . . 7
⊢
((∀𝑥(𝑥 ∈ 𝐵 → ¬ 𝜑) ∧ (𝑥 ∈ 𝐴 ∧ 𝜑)) → 𝜑) |
| 12 | 10, 11 | jca 511 |
. . . . . 6
⊢
((∀𝑥(𝑥 ∈ 𝐵 → ¬ 𝜑) ∧ (𝑥 ∈ 𝐴 ∧ 𝜑)) → (𝑥 ∈ (𝐴 ∖ 𝐵) ∧ 𝜑)) |
| 13 | 12 | ex 412 |
. . . . 5
⊢
(∀𝑥(𝑥 ∈ 𝐵 → ¬ 𝜑) → ((𝑥 ∈ 𝐴 ∧ 𝜑) → (𝑥 ∈ (𝐴 ∖ 𝐵) ∧ 𝜑))) |
| 14 | 3, 13 | eximd 2216 |
. . . 4
⊢
(∀𝑥(𝑥 ∈ 𝐵 → ¬ 𝜑) → (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) → ∃𝑥(𝑥 ∈ (𝐴 ∖ 𝐵) ∧ 𝜑))) |
| 15 | 14 | impcom 407 |
. . 3
⊢
((∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ∧ ∀𝑥(𝑥 ∈ 𝐵 → ¬ 𝜑)) → ∃𝑥(𝑥 ∈ (𝐴 ∖ 𝐵) ∧ 𝜑)) |
| 16 | 1, 2, 15 | syl2anb 598 |
. 2
⊢
((∃𝑥 ∈
𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐵 ¬ 𝜑) → ∃𝑥(𝑥 ∈ (𝐴 ∖ 𝐵) ∧ 𝜑)) |
| 17 | | df-rex 3071 |
. 2
⊢
(∃𝑥 ∈
(𝐴 ∖ 𝐵)𝜑 ↔ ∃𝑥(𝑥 ∈ (𝐴 ∖ 𝐵) ∧ 𝜑)) |
| 18 | 16, 17 | sylibr 234 |
1
⊢
((∃𝑥 ∈
𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐵 ¬ 𝜑) → ∃𝑥 ∈ (𝐴 ∖ 𝐵)𝜑) |