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	⊢ Ⅎ 𝑦 𝐴
	nfdisj.2	⊢ Ⅎ 𝑦 𝐵
Assertion	nfdisj	⊢ Ⅎ 𝑦 Disj 𝑥 ∈ 𝐴 𝐵

Proof

Step	Hyp	Ref	Expression
1		nfdisj.1	⊢ Ⅎ 𝑦 𝐴
2		nfdisj.2	⊢ Ⅎ 𝑦 𝐵
3		dfdisj2	⊢ ( Disj 𝑥 ∈ 𝐴 𝐵 ↔ ∀ 𝑧 ∃* 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵 ) )
4		nftru	⊢ Ⅎ 𝑥 ⊤
5		nfcvf	⊢ ( ¬ ∀ 𝑦 𝑦 = 𝑥 → Ⅎ 𝑦 𝑥 )
6	1	a1i	⊢ ( ¬ ∀ 𝑦 𝑦 = 𝑥 → Ⅎ 𝑦 𝐴 )
7	5 6	nfeld	⊢ ( ¬ ∀ 𝑦 𝑦 = 𝑥 → Ⅎ 𝑦 𝑥 ∈ 𝐴 )
8	2	nfcri	⊢ Ⅎ 𝑦 𝑧 ∈ 𝐵
9	8	a1i	⊢ ( ¬ ∀ 𝑦 𝑦 = 𝑥 → Ⅎ 𝑦 𝑧 ∈ 𝐵 )
10	7 9	nfand	⊢ ( ¬ ∀ 𝑦 𝑦 = 𝑥 → Ⅎ 𝑦 ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵 ) )
11	10	adantl	⊢ ( ( ⊤ ∧ ¬ ∀ 𝑦 𝑦 = 𝑥 ) → Ⅎ 𝑦 ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵 ) )
12	4 11	nfmod2	⊢ ( ⊤ → Ⅎ 𝑦 ∃* 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵 ) )
13	12	mptru	⊢ Ⅎ 𝑦 ∃* 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵 )
14	13	nfal	⊢ Ⅎ 𝑦 ∀ 𝑧 ∃* 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵 )
15	3 14	nfxfr	⊢ Ⅎ 𝑦 Disj 𝑥 ∈ 𝐴 𝐵