Database
ZF (ZERMELO-FRAENKEL) SET THEORY
ZF Set Theory - start with the Axiom of Extensionality
The difference, union, and intersection of two classes
The intersection of two classes
nfin
Metamath Proof Explorer
Description: Bound-variable hypothesis builder for the intersection of classes.
(Contributed by NM , 15-Sep-2003) (Revised by Mario Carneiro , 14-Oct-2016)

Ref
Expression
Hypotheses
nfin.1
⊢ Ⅎ 𝑥 𝐴
nfin.2
⊢ Ⅎ 𝑥 𝐵
Assertion
nfin
⊢ Ⅎ 𝑥 ( 𝐴 ∩ 𝐵 )

Proof
Step
Hyp
Ref
Expression
1
nfin.1
⊢ Ⅎ 𝑥 𝐴
2
nfin.2
⊢ Ⅎ 𝑥 𝐵
3
dfin5
⊢ ( 𝐴 ∩ 𝐵 ) = { 𝑦 ∈ 𝐴 ∣ 𝑦 ∈ 𝐵 }
4
2
nfcri
⊢ Ⅎ 𝑥 𝑦 ∈ 𝐵
5
4 1
nfrabw
⊢ Ⅎ 𝑥 { 𝑦 ∈ 𝐴 ∣ 𝑦 ∈ 𝐵 }
6
3 5
nfcxfr
⊢ Ⅎ 𝑥 ( 𝐴 ∩ 𝐵 )