Theorem nfdisj1

Description: Bound-variable hypothesis builder for disjoint collection. (Contributed by Mario Carneiro, 14-Nov-2016)

	Ref	Expression
Assertion	nfdisj1	⊢ Ⅎ 𝑥 Disj 𝑥 ∈ 𝐴 𝐵

Proof

Step	Hyp	Ref	Expression
1		df-disj	⊢ ( Disj 𝑥 ∈ 𝐴 𝐵 ↔ ∀ 𝑦 ∃* 𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 )
2		nfrmo1	⊢ Ⅎ 𝑥 ∃* 𝑥 ∈ 𝐴 𝑦 ∈ 𝐵
3	2	nfal	⊢ Ⅎ 𝑥 ∀ 𝑦 ∃* 𝑥 ∈ 𝐴 𝑦 ∈ 𝐵
4	1 3	nfxfr	⊢ Ⅎ 𝑥 Disj 𝑥 ∈ 𝐴 𝐵