Metamath Proof Explorer

Theorem nfdisj1

Description: Bound-variable hypothesis builder for disjoint collection. (Contributed by Mario Carneiro, 14-Nov-2016)

Ref Expression
Assertion nfdisj1 
|- F/ x Disj_ x e. A B

Proof

Step Hyp Ref Expression
1 df-disj 
 |-  ( Disj_ x e. A B <-> A. y E* x e. A y e. B )
2 nfrmo1 
 |-  F/ x E* x e. A y e. B
3 2 nfal 
 |-  F/ x A. y E* x e. A y e. B
4 1 3 nfxfr 
 |-  F/ x Disj_ x e. A B