Theorem nfdisj

Description: Bound-variable hypothesis builder for disjoint collection. Usage of this theorem is discouraged because it depends on ax-13 . Use the weaker nfdisjw when possible. (Contributed by Mario Carneiro, 14-Nov-2016) (New usage is discouraged.)

	Ref	Expression
Hypotheses	nfdisj.1	|- F/_ y A
	nfdisj.2	|- F/_ y B
Assertion	nfdisj	|- F/ y Disj_ x e. A B

Proof

Step	Hyp	Ref	Expression
1		nfdisj.1	|- F/_ y A
2		nfdisj.2	|- F/_ y B
3		dfdisj2	|- ( Disj_ x e. A B <-> A. z E* x ( x e. A /\ z e. B ) )
4		nftru	|- F/ x T.
5		nfcvf	|- ( -. A. y y = x -> F/_ y x )
6	1	a1i	|- ( -. A. y y = x -> F/_ y A )
7	5 6	nfeld	|- ( -. A. y y = x -> F/ y x e. A )
8	2	nfcri	|- F/ y z e. B
9	8	a1i	|- ( -. A. y y = x -> F/ y z e. B )
10	7 9	nfand	|- ( -. A. y y = x -> F/ y ( x e. A /\ z e. B ) )
11	10	adantl	|- ( ( T. /\ -. A. y y = x ) -> F/ y ( x e. A /\ z e. B ) )
12	4 11	nfmod2	|- ( T. -> F/ y E* x ( x e. A /\ z e. B ) )
13	12	mptru	|- F/ y E* x ( x e. A /\ z e. B )
14	13	nfal	|- F/ y A. z E* x ( x e. A /\ z e. B )
15	3 14	nfxfr	|- F/ y Disj_ x e. A B