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	$$⊢\underset{\_}{Ⅎ}yA$$
	nfdisj.2	$$⊢\underset{\_}{Ⅎ}yB$$
Assertion	nfdisj	$$⊢Ⅎy\underset{x\in A}{Disj}B$$

Proof

Step	Hyp	Ref	Expression
1		nfdisj.1	$$⊢\underset{\_}{Ⅎ}yA$$
2		nfdisj.2	$$⊢\underset{\_}{Ⅎ}yB$$
3		dfdisj2	$$⊢\underset{x\in A}{Disj}B\leftrightarrow \forall z{\exists }^{*}x\left(x\in A\wedge z\in B\right)$$
4		nftru	$$⊢Ⅎx\top$$
5		nfcvf	$$⊢\neg \forall yy=x\to \underset{\_}{Ⅎ}yx$$
6	1	a1i	$$⊢\neg \forall yy=x\to \underset{\_}{Ⅎ}yA$$
7	5 6	nfeld	$$⊢\neg \forall yy=x\to Ⅎyx\in A$$
8	2	nfcri	$$⊢Ⅎyz\in B$$
9	8	a1i	$$⊢\neg \forall yy=x\to Ⅎyz\in B$$
10	7 9	nfand	$$⊢\neg \forall yy=x\to Ⅎy\left(x\in A\wedge z\in B\right)$$
11	10	adantl	$$⊢\left(\top \wedge \neg \forall yy=x\right)\to Ⅎy\left(x\in A\wedge z\in B\right)$$
12	4 11	nfmod2	$$⊢\top \to Ⅎy{\exists }^{*}x\left(x\in A\wedge z\in B\right)$$
13	12	mptru	$$⊢Ⅎy{\exists }^{*}x\left(x\in A\wedge z\in B\right)$$
14	13	nfal	$$⊢Ⅎy\forall z{\exists }^{*}x\left(x\in A\wedge z\in B\right)$$
15	3 14	nfxfr	$$⊢Ⅎy\underset{x\in A}{Disj}B$$