Theorem disjOLD

Description: Obsolete version of disj as of 28-Jun-2024. (Contributed by NM, 17-Feb-2004) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	disjOLD	⊢ ( ( 𝐴 ∩ 𝐵 ) = ∅ ↔ ∀ 𝑥 ∈ 𝐴 ¬ 𝑥 ∈ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		df-in	⊢ ( 𝐴 ∩ 𝐵 ) = { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) }
2	1	eqeq1i	⊢ ( ( 𝐴 ∩ 𝐵 ) = ∅ ↔ { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) } = ∅ )
3		abeq1	⊢ ( { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) } = ∅ ↔ ∀ 𝑥 ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) ↔ 𝑥 ∈ ∅ ) )
4		imnan	⊢ ( ( 𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ 𝐵 ) ↔ ¬ ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) )
5		noel	⊢ ¬ 𝑥 ∈ ∅
6	5	nbn	⊢ ( ¬ ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) ↔ ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) ↔ 𝑥 ∈ ∅ ) )
7	4 6	bitr2i	⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) ↔ 𝑥 ∈ ∅ ) ↔ ( 𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ 𝐵 ) )
8	7	albii	⊢ ( ∀ 𝑥 ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) ↔ 𝑥 ∈ ∅ ) ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ 𝐵 ) )
9	2 3 8	3bitri	⊢ ( ( 𝐴 ∩ 𝐵 ) = ∅ ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ 𝐵 ) )
10		df-ral	⊢ ( ∀ 𝑥 ∈ 𝐴 ¬ 𝑥 ∈ 𝐵 ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ 𝐵 ) )
11	9 10	bitr4i	⊢ ( ( 𝐴 ∩ 𝐵 ) = ∅ ↔ ∀ 𝑥 ∈ 𝐴 ¬ 𝑥 ∈ 𝐵 )