Theorem qseq

Description: The quotient set equal to a class.

This theorem is used when a class A is identified with a quotient ( dom R /. R ) . In such a situation, every element u e. A is an R-coset [ v ] R for some v e. dom R , but there is no requirement that the "witness" v be equal to its own block [ v ] R . A is a set of blocks (equivalence classes), not a set of raw witnesses. In particular, when ( dom R /. R ) = A is read together with a partition hypothesis R Part A (defined as dfpart2 ), A is being treated as the set of blocks [ v ] R ; it does not assert any fixed-point condition v = [ v ] R such as would arise from the mistaken reading u e. A <-> u = [ u ] R . Cf. dmqsblocks . (Contributed by Peter Mazsa, 19-Oct-2018)

	Ref	Expression
Assertion	qseq	$$⊢B/R=A\leftrightarrow \forall u\left(u\in A\leftrightarrow \exists v\in Bu=\left[v\right]R\right)$$

Proof

Step	Hyp	Ref	Expression
1		df-qs	$$⊢B/R=\left\{u|\exists v\in Bu=\left[v\right]R\right\}$$
2	1	eqeq2i	$$⊢A=B/R\leftrightarrow A=\left\{u|\exists v\in Bu=\left[v\right]R\right\}$$
3		eqcom	$$⊢A=B/R\leftrightarrow B/R=A$$
4		eqabb	$$⊢A=\left\{u|\exists v\in Bu=\left[v\right]R\right\}\leftrightarrow \forall u\left(u\in A\leftrightarrow \exists v\in Bu=\left[v\right]R\right)$$
5	2 3 4	3bitr3i	$$⊢B/R=A\leftrightarrow \forall u\left(u\in A\leftrightarrow \exists v\in Bu=\left[v\right]R\right)$$