Theorem dfdisj2

Description: Alternate definition for disjoint classes. (Contributed by NM, 17-Jun-2017)

	Ref	Expression
Assertion	dfdisj2	⊢ ( Disj 𝑥 ∈ 𝐴 𝐵 ↔ ∀ 𝑦 ∃* 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		df-disj	⊢ ( Disj 𝑥 ∈ 𝐴 𝐵 ↔ ∀ 𝑦 ∃* 𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 )
2		df-rmo	⊢ ( ∃* 𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 ↔ ∃* 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) )
3	2	albii	⊢ ( ∀ 𝑦 ∃* 𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 ↔ ∀ 𝑦 ∃* 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) )
4	1 3	bitri	⊢ ( Disj 𝑥 ∈ 𝐴 𝐵 ↔ ∀ 𝑦 ∃* 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) )