Metamath Proof Explorer


Definition df-dmqss

Description: Define the class of domain quotients. Domain quotients are pairs of sets, typically a relation and a set, where the quotient (see df-qs ) of the relation on its domain is equal to the set. See comments of df-ers for the motivation for this definition. (Contributed by Peter Mazsa, 16-Apr-2019)

Ref Expression
Assertion df-dmqss DomainQss = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( dom 𝑥 / 𝑥 ) = 𝑦 }

Detailed syntax breakdown

Step Hyp Ref Expression
0 cdmqss DomainQss
1 vx 𝑥
2 vy 𝑦
3 1 cv 𝑥
4 3 cdm dom 𝑥
5 4 3 cqs ( dom 𝑥 / 𝑥 )
6 2 cv 𝑦
7 5 6 wceq ( dom 𝑥 / 𝑥 ) = 𝑦
8 7 1 2 copab { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( dom 𝑥 / 𝑥 ) = 𝑦 }
9 0 8 wceq DomainQss = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( dom 𝑥 / 𝑥 ) = 𝑦 }