Theorem disjeccnvep

Description: Property of the epsilon relation. (Contributed by Peter Mazsa, 27-Apr-2020)

	Ref	Expression
Assertion	disjeccnvep	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ( [ 𝐴 ] ◡ E ∩ [ 𝐵 ] ◡ E ) = ∅ ↔ ( 𝐴 ∩ 𝐵 ) = ∅ ) )

Proof

Step	Hyp	Ref	Expression
1		eccnvep	⊢ ( 𝐴 ∈ 𝑉 → [ 𝐴 ] ◡ E = 𝐴 )
2		eccnvep	⊢ ( 𝐵 ∈ 𝑊 → [ 𝐵 ] ◡ E = 𝐵 )
3	1 2	ineqan12d	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( [ 𝐴 ] ◡ E ∩ [ 𝐵 ] ◡ E ) = ( 𝐴 ∩ 𝐵 ) )
4	3	eqeq1d	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ( [ 𝐴 ] ◡ E ∩ [ 𝐵 ] ◡ E ) = ∅ ↔ ( 𝐴 ∩ 𝐵 ) = ∅ ) )