Step |
Hyp |
Ref |
Expression |
1 |
|
n0 |
⊢ ( 𝐴 ≠ ∅ ↔ ∃ 𝑥 𝑥 ∈ 𝐴 ) |
2 |
1
|
biimpi |
⊢ ( 𝐴 ≠ ∅ → ∃ 𝑥 𝑥 ∈ 𝐴 ) |
3 |
2
|
anim2i |
⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐴 ≠ ∅ ) → ( 𝐴 ∈ 𝑉 ∧ ∃ 𝑥 𝑥 ∈ 𝐴 ) ) |
4 |
|
zfregcl |
⊢ ( 𝐴 ∈ 𝑉 → ( ∃ 𝑥 𝑥 ∈ 𝐴 → ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝑥 ¬ 𝑦 ∈ 𝐴 ) ) |
5 |
4
|
imp |
⊢ ( ( 𝐴 ∈ 𝑉 ∧ ∃ 𝑥 𝑥 ∈ 𝐴 ) → ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝑥 ¬ 𝑦 ∈ 𝐴 ) |
6 |
|
disj |
⊢ ( ( 𝑥 ∩ 𝐴 ) = ∅ ↔ ∀ 𝑦 ∈ 𝑥 ¬ 𝑦 ∈ 𝐴 ) |
7 |
6
|
rexbii |
⊢ ( ∃ 𝑥 ∈ 𝐴 ( 𝑥 ∩ 𝐴 ) = ∅ ↔ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝑥 ¬ 𝑦 ∈ 𝐴 ) |
8 |
7
|
biimpri |
⊢ ( ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝑥 ¬ 𝑦 ∈ 𝐴 → ∃ 𝑥 ∈ 𝐴 ( 𝑥 ∩ 𝐴 ) = ∅ ) |
9 |
3 5 8
|
3syl |
⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐴 ≠ ∅ ) → ∃ 𝑥 ∈ 𝐴 ( 𝑥 ∩ 𝐴 ) = ∅ ) |