This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
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
Description: Bound-variable hypothesis builder for the intersection of classes.
(Contributed by NM , 15-Sep-2003) (Revised by Mario Carneiro , 14-Oct-2016) Avoid ax-10 , ax-11 , ax-12 . (Revised by SN , 14-May-2025)
Ref
Expression
Hypotheses
nfin.1 ⊢ Ⅎ 𝑥 𝐴
nfin.2 ⊢ Ⅎ 𝑥 𝐵
Assertion
nfin ⊢ Ⅎ 𝑥 ( 𝐴 ∩ 𝐵 )
Proof
Step
Hyp
Ref
Expression
1
nfin.1 ⊢ Ⅎ 𝑥 𝐴
2
nfin.2 ⊢ Ⅎ 𝑥 𝐵
3
elin ⊢ ( 𝑦 ∈ ( 𝐴 ∩ 𝐵 ) ↔ ( 𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) )
4
1
nfcri ⊢ Ⅎ 𝑥 𝑦 ∈ 𝐴
5
2
nfcri ⊢ Ⅎ 𝑥 𝑦 ∈ 𝐵
6
4 5
nfan ⊢ Ⅎ 𝑥 ( 𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 )
7
3 6
nfxfr ⊢ Ⅎ 𝑥 𝑦 ∈ ( 𝐴 ∩ 𝐵 )
8
7
nfci ⊢ Ⅎ 𝑥 ( 𝐴 ∩ 𝐵 )