Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Peter Mazsa
Disjoints vs. converse functions
eleldisjs
Next ⟩
eleldisjseldisj
Metamath Proof Explorer
Ascii
Unicode
Theorem
eleldisjs
Description:
Elementhood in the disjoint elements class.
(Contributed by
Peter Mazsa
, 23-Jul-2023)
Ref
Expression
Assertion
eleldisjs
⊢
A
∈
V
→
A
∈
ElDisjs
↔
E
-1
↾
A
∈
Disjs
Proof
Step
Hyp
Ref
Expression
1
reseq2
⊢
a
=
A
→
E
-1
↾
a
=
E
-1
↾
A
2
1
eleq1d
⊢
a
=
A
→
E
-1
↾
a
∈
Disjs
↔
E
-1
↾
A
∈
Disjs
3
df-eldisjs
⊢
ElDisjs
=
a
|
E
-1
↾
a
∈
Disjs
4
2
3
elab2g
⊢
A
∈
V
→
A
∈
ElDisjs
↔
E
-1
↾
A
∈
Disjs