Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Peter Mazsa
Disjoints vs. converse functions
eldisjeq
Next ⟩
eldisjeqi
Metamath Proof Explorer
Ascii
Unicode
Theorem
eldisjeq
Description:
Equality theorem for disjoint elementhood.
(Contributed by
Peter Mazsa
, 23-Sep-2021)
Ref
Expression
Assertion
eldisjeq
⊢
A
=
B
→
ElDisj
A
↔
ElDisj
B
Proof
Step
Hyp
Ref
Expression
1
reseq2
⊢
A
=
B
→
E
-1
↾
A
=
E
-1
↾
B
2
1
disjeqd
⊢
A
=
B
→
Disj
E
-1
↾
A
↔
Disj
E
-1
↾
B
3
df-eldisj
⊢
ElDisj
A
↔
Disj
E
-1
↾
A
4
df-eldisj
⊢
ElDisj
B
↔
Disj
E
-1
↾
B
5
2
3
4
3bitr4g
⊢
A
=
B
→
ElDisj
A
↔
ElDisj
B