Database
ZF (ZERMELO-FRAENKEL) SET THEORY
ZF Set Theory - start with the Axiom of Extensionality
The intersection of a class
elrint
Next ⟩
elrint2
Metamath Proof Explorer
Ascii
Unicode
Theorem
elrint
Description:
Membership in a restricted intersection.
(Contributed by
Stefan O'Rear
, 3-Apr-2015)
Ref
Expression
Assertion
elrint
⊢
X
∈
A
∩
⋂
B
↔
X
∈
A
∧
∀
y
∈
B
X
∈
y
Proof
Step
Hyp
Ref
Expression
1
elin
⊢
X
∈
A
∩
⋂
B
↔
X
∈
A
∧
X
∈
⋂
B
2
elintg
⊢
X
∈
A
→
X
∈
⋂
B
↔
∀
y
∈
B
X
∈
y
3
2
pm5.32i
⊢
X
∈
A
∧
X
∈
⋂
B
↔
X
∈
A
∧
∀
y
∈
B
X
∈
y
4
1
3
bitri
⊢
X
∈
A
∩
⋂
B
↔
X
∈
A
∧
∀
y
∈
B
X
∈
y