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

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 𝑥 / 𝑥 ) = 𝑦 }