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

Proof

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

Metamath Proof Explorer

Theorem nfdisj

Proof