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	\|- F/_ y A
	nfdisjw.2	\|- F/_ y B
Assertion	nfdisjw	\|- F/ y Disj_ x e. A B

Proof

Step	Hyp	Ref	Expression
1		nfdisjw.1	\|- F/_ y A
2		nfdisjw.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		nfcvd	\|- ( T. -> F/_ y x )
6	1	a1i	\|- ( T. -> F/_ y A )
7	5 6	nfeld	\|- ( T. -> F/ y x e. A )
8	2	nfcri	\|- F/ y z e. B
9	8	a1i	\|- ( T. -> F/ y z e. B )
10	7 9	nfand	\|- ( T. -> F/ y ( x e. A /\ z e. B ) )
11	4 10	nfmodv	\|- ( T. -> F/ y E* x ( x e. A /\ z e. B ) )
12	11	mptru	\|- F/ y E* x ( x e. A /\ z e. B )
13	12	nfal	\|- F/ y A. z E* x ( x e. A /\ z e. B )
14	3 13	nfxfr	\|- F/ y Disj_ x e. A B

Metamath Proof Explorer

Theorem nfdisjw

Proof