Theorem eldisjeq

Description: Equality theorem for disjoint elementhood. (Contributed by Peter Mazsa, 23-Sep-2021)

	Ref	Expression
Assertion	eldisjeq	⊢ ( 𝐴 = 𝐵 → ( ElDisj 𝐴 ↔ ElDisj 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		reseq2	⊢ ( 𝐴 = 𝐵 → ( ◡ E ↾ 𝐴 ) = ( ◡ E ↾ 𝐵 ) )
2	1	disjeqd	⊢ ( 𝐴 = 𝐵 → ( Disj ( ◡ E ↾ 𝐴 ) ↔ Disj ( ◡ E ↾ 𝐵 ) ) )
3		df-eldisj	⊢ ( ElDisj 𝐴 ↔ Disj ( ◡ E ↾ 𝐴 ) )
4		df-eldisj	⊢ ( ElDisj 𝐵 ↔ Disj ( ◡ E ↾ 𝐵 ) )
5	2 3 4	3bitr4g	⊢ ( 𝐴 = 𝐵 → ( ElDisj 𝐴 ↔ ElDisj 𝐵 ) )