Metamath Proof Explorer


Theorem nfdisj1

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

Ref Expression
Assertion nfdisj1 x Disj x A B

Proof

Step Hyp Ref Expression
1 df-disj Disj x A B y * x A y B
2 nfrmo1 x * x A y B
3 2 nfal x y * x A y B
4 1 3 nfxfr x Disj x A B