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

Metamath Proof Explorer

Definition df-membparts

Description: Define the class of member partition relations on their domain quotients. (Contributed by Peter Mazsa, 26-Jun-2021)

Ref Expression
Assertion df-membparts MembParts = { 𝑎 ∣ ( ◡ E ↾ 𝑎 ) Parts 𝑎 }

Detailed syntax breakdown

Step Hyp Ref Expression
0 cmembparts ⊢ MembParts
1 va ⊢ 𝑎
2 cep ⊢ E
3 2 ccnv ⊢ ◡ E
4 1 cv ⊢ 𝑎
5 3 4 cres ⊢ ( ◡ E ↾ 𝑎 )
6 cparts ⊢ Parts
7 5 4 6 wbr ⊢ ( ◡ E ↾ 𝑎 ) Parts 𝑎
8 7 1 cab ⊢ { 𝑎 ∣ ( ◡ E ↾ 𝑎 ) Parts 𝑎 }
9 0 8 wceq ⊢ MembParts = { 𝑎 ∣ ( ◡ E ↾ 𝑎 ) Parts 𝑎 }