Metamath Proof Explorer


Theorem nfiin

Description: Bound-variable hypothesis builder for indexed intersection. (Contributed by Mario Carneiro, 25-Jan-2014) Add disjoint variable condition to avoid ax-13 . See nfiing for a less restrictive version requiring more axioms. (Revised by Gino Giotto, 20-Jan-2024)

Ref Expression
Hypotheses nfiun.1 _yA
nfiun.2 _yB
Assertion nfiin _yxAB

Proof

Step Hyp Ref Expression
1 nfiun.1 _yA
2 nfiun.2 _yB
3 df-iin xAB=z|xAzB
4 2 nfcri yzB
5 1 4 nfralw yxAzB
6 5 nfab _yz|xAzB
7 3 6 nfcxfr _yxAB