Database
ZF (ZERMELO-FRAENKEL) SET THEORY
ZF Set Theory - start with the Axiom of Extensionality
The intersection of a class
elint
Next ⟩
elint2
Metamath Proof Explorer
Ascii
Unicode
Theorem
elint
Description:
Membership in class intersection.
(Contributed by
NM
, 21-May-1994)
Ref
Expression
Hypothesis
elint.1
⊢
A
∈
V
Assertion
elint
⊢
A
∈
⋂
B
↔
∀
x
x
∈
B
→
A
∈
x
Proof
Step
Hyp
Ref
Expression
1
elint.1
⊢
A
∈
V
2
eleq1
⊢
z
=
y
→
z
∈
x
↔
y
∈
x
3
2
imbi2d
⊢
z
=
y
→
x
∈
B
→
z
∈
x
↔
x
∈
B
→
y
∈
x
4
3
albidv
⊢
z
=
y
→
∀
x
x
∈
B
→
z
∈
x
↔
∀
x
x
∈
B
→
y
∈
x
5
eleq1
⊢
y
=
A
→
y
∈
x
↔
A
∈
x
6
5
imbi2d
⊢
y
=
A
→
x
∈
B
→
y
∈
x
↔
x
∈
B
→
A
∈
x
7
6
albidv
⊢
y
=
A
→
∀
x
x
∈
B
→
y
∈
x
↔
∀
x
x
∈
B
→
A
∈
x
8
df-int
⊢
⋂
B
=
z
|
∀
x
x
∈
B
→
z
∈
x
9
4
7
8
elab2gw
⊢
A
∈
V
→
A
∈
⋂
B
↔
∀
x
x
∈
B
→
A
∈
x
10
1
9
ax-mp
⊢
A
∈
⋂
B
↔
∀
x
x
∈
B
→
A
∈
x