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 <-> A. u ( u e. A <-> E. v e. B u = [ v ] R ) )

Proof

Step	Hyp	Ref	Expression
1		df-qs	|- ( B /. R ) = { u | E. v e. B u = [ v ] R }
2	1	eqeq2i	|- ( A = ( B /. R ) <-> A = { u | E. v e. B u = [ v ] R } )
3		eqcom	|- ( A = ( B /. R ) <-> ( B /. R ) = A )
4		eqabb	|- ( A = { u | E. v e. B u = [ v ] R } <-> A. u ( u e. A <-> E. v e. B u = [ v ] R ) )
5	2 3 4	3bitr3i	|- ( ( B /. R ) = A <-> A. u ( u e. A <-> E. v e. B u = [ v ] R ) )