Theorem eldisjn0elb

Description: Two forms of disjoint elements when the empty set is not an element of the class. (Contributed by Peter Mazsa, 31-Dec-2024)

	Ref	Expression
Assertion	eldisjn0elb	⊢ ( ( ElDisj 𝐴 ∧ ¬ ∅ ∈ 𝐴 ) ↔ ( Disj ( ◡ E ↾ 𝐴 ) ∧ ( dom ( ◡ E ↾ 𝐴 ) / ( ◡ E ↾ 𝐴 ) ) = 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		df-eldisj	⊢ ( ElDisj 𝐴 ↔ Disj ( ◡ E ↾ 𝐴 ) )
2		n0el3	⊢ ( ¬ ∅ ∈ 𝐴 ↔ ( dom ( ◡ E ↾ 𝐴 ) / ( ◡ E ↾ 𝐴 ) ) = 𝐴 )
3	1 2	anbi12i	⊢ ( ( ElDisj 𝐴 ∧ ¬ ∅ ∈ 𝐴 ) ↔ ( Disj ( ◡ E ↾ 𝐴 ) ∧ ( dom ( ◡ E ↾ 𝐴 ) / ( ◡ E ↾ 𝐴 ) ) = 𝐴 ) )