Step |
Hyp |
Ref |
Expression |
1 |
|
elint.1 |
⊢ 𝐴 ∈ V |
2 |
|
eleq1 |
⊢ ( 𝑧 = 𝑦 → ( 𝑧 ∈ 𝑥 ↔ 𝑦 ∈ 𝑥 ) ) |
3 |
2
|
imbi2d |
⊢ ( 𝑧 = 𝑦 → ( ( 𝑥 ∈ 𝐵 → 𝑧 ∈ 𝑥 ) ↔ ( 𝑥 ∈ 𝐵 → 𝑦 ∈ 𝑥 ) ) ) |
4 |
3
|
albidv |
⊢ ( 𝑧 = 𝑦 → ( ∀ 𝑥 ( 𝑥 ∈ 𝐵 → 𝑧 ∈ 𝑥 ) ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐵 → 𝑦 ∈ 𝑥 ) ) ) |
5 |
|
eleq1 |
⊢ ( 𝑦 = 𝐴 → ( 𝑦 ∈ 𝑥 ↔ 𝐴 ∈ 𝑥 ) ) |
6 |
5
|
imbi2d |
⊢ ( 𝑦 = 𝐴 → ( ( 𝑥 ∈ 𝐵 → 𝑦 ∈ 𝑥 ) ↔ ( 𝑥 ∈ 𝐵 → 𝐴 ∈ 𝑥 ) ) ) |
7 |
6
|
albidv |
⊢ ( 𝑦 = 𝐴 → ( ∀ 𝑥 ( 𝑥 ∈ 𝐵 → 𝑦 ∈ 𝑥 ) ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐵 → 𝐴 ∈ 𝑥 ) ) ) |
8 |
|
df-int |
⊢ ∩ 𝐵 = { 𝑧 ∣ ∀ 𝑥 ( 𝑥 ∈ 𝐵 → 𝑧 ∈ 𝑥 ) } |
9 |
4 7 8
|
elab2gw |
⊢ ( 𝐴 ∈ V → ( 𝐴 ∈ ∩ 𝐵 ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐵 → 𝐴 ∈ 𝑥 ) ) ) |
10 |
1 9
|
ax-mp |
⊢ ( 𝐴 ∈ ∩ 𝐵 ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐵 → 𝐴 ∈ 𝑥 ) ) |