This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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

Proof

Step	Hyp	Ref	Expression
1		nfdisjw.1	$⊢ \underline{Ⅎ} y A$
2		nfdisjw.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		nfcvd	$⊢ ⊤ \to \underline{Ⅎ} y x$
6	1	a1i	$⊢ ⊤ \to \underline{Ⅎ} y A$
7	5 6	nfeld	$⊢ ⊤ \to Ⅎ y x \in A$
8	2	nfcri	$⊢ Ⅎ y z \in B$
9	8	a1i	$⊢ ⊤ \to Ⅎ y z \in B$
10	7 9	nfand	$⊢ ⊤ \to Ⅎ y (x \in A \land z \in B)$
11	4 10	nfmodv	$⊢ ⊤ \to Ⅎ y \exists^{*} x (x \in A \land z \in B)$
12	11	mptru	$⊢ Ⅎ y \exists^{*} x (x \in A \land z \in B)$
13	12	nfal	$⊢ Ⅎ y \forall z \exists^{*} x (x \in A \land z \in B)$
14	3 13	nfxfr	$⊢ Ⅎ y \underset{x \in A}{Disj} B$