Theorem nfdisjw

Description: Bound-variable hypothesis builder for disjoint collection. Version of nfdisj with a disjoint variable condition, which does not require ax-13 . (Contributed by Mario Carneiro, 14-Nov-2016) Avoid ax-13 . (Revised by GG, 26-Jan-2024)

	Ref	Expression
Hypotheses	nfdisjw.1	$$⊢\underset{\_}{Ⅎ}yA$$
	nfdisjw.2	$$⊢\underset{\_}{Ⅎ}yB$$
Assertion	nfdisjw	$$⊢Ⅎy\underset{x\in A}{Disj}B$$

Proof

Step	Hyp	Ref	Expression
1		nfdisjw.1	$$⊢\underset{\_}{Ⅎ}yA$$
2		nfdisjw.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	1	a1i	$$⊢\top \to \underset{\_}{Ⅎ}yA$$
6	5	nfcrd	$$⊢\top \to Ⅎyx\in A$$
7	2	nfcri	$$⊢Ⅎyz\in B$$
8	7	a1i	$$⊢\top \to Ⅎyz\in B$$
9	6 8	nfand	$$⊢\top \to Ⅎy\left(x\in A\wedge z\in B\right)$$
10	4 9	nfmodv	$$⊢\top \to Ⅎy{\exists }^{*}x\left(x\in A\wedge z\in B\right)$$
11	10	mptru	$$⊢Ⅎy{\exists }^{*}x\left(x\in A\wedge z\in B\right)$$
12	11	nfal	$$⊢Ⅎy\forall z{\exists }^{*}x\left(x\in A\wedge z\in B\right)$$
13	3 12	nfxfr	$$⊢Ⅎy\underset{x\in A}{Disj}B$$