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 = { 𝑎 ∣ ( ◡ E ↾ 𝑎 ) ∈ Disjs }

Detailed syntax breakdown

Step Hyp Ref Expression
0 celdisjs ⊢ ElDisjs
1 va ⊢ 𝑎
2 cep ⊢ E
3 2 ccnv ⊢ ◡ E
4 1 cv ⊢ 𝑎
5 3 4 cres ⊢ ( ◡ E ↾ 𝑎 )
6 cdisjs ⊢ Disjs
7 5 6 wcel ⊢ ( ◡ E ↾ 𝑎 ) ∈ Disjs
8 7 1 cab ⊢ { 𝑎 ∣ ( ◡ E ↾ 𝑎 ) ∈ Disjs }
9 0 8 wceq ⊢ ElDisjs = { 𝑎 ∣ ( ◡ E ↾ 𝑎 ) ∈ Disjs }