This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Definition df-eldisjs

Description: Define the disjoint element relations class, i.e., the disjoint elements class. The element of the disjoint elements class and the disjoint elementhood predicate are the same, that is ( A e. ElDisjs <-> ElDisj A ) when A is a set, see eleldisjseldisj . (Contributed by Peter Mazsa, 28-Nov-2022)

Ref Expression
Assertion df-eldisjs 
|- ElDisjs = { a | ( `' _E |` a ) e. Disjs }

Detailed syntax breakdown

Step Hyp Ref Expression
0 celdisjs 
 |-  ElDisjs
1 va 
 |-  a
2 cep 
 |-  _E
3 2 ccnv 
 |-  `' _E
4 1 cv 
 |-  a
5 3 4 cres 
 |-  ( `' _E |` a )
6 cdisjs 
 |-  Disjs
7 5 6 wcel 
 |-  ( `' _E |` a ) e. Disjs
8 7 1 cab 
 |-  { a | ( `' _E |` a ) e. Disjs }
9 0 8 wceq 
 |-  ElDisjs = { a | ( `' _E |` a ) e. Disjs }