Theorem dfcnqs 11122

Description: Technical trick to permit reuse of previous lemmas to prove arithmetic operation laws in ℂ from those in R. The trick involves qsid 8775, which shows that the coset of the converse membership relation (which is not an equivalence relation) acts as an identity divisor for the quotient set operation. This lets us "pretend" that ℂ is a quotient set, even though it is not (compare df-c 11101), and allows to reuse some of the equivalence class lemmas we developed for the transition from positive reals to signed reals, etc. (Contributed by NM, 13-Aug-1995.) (New usage is discouraged.)

Assertion

Ref	Expression
dfcnqs	⊢ ℂ = ((R × R) / ◡ E )

Proof of Theorem dfcnqs

Step	Hyp	Ref	Expression
1		df-c 11101	. 2 ⊢ ℂ = (R × R)
2		qsid 8775	. 2 ⊢ ((R × R) / ◡ E ) = (R × R)
3	1, 2	eqtr4i 2789	1 ⊢ ℂ = ((R × R) / ◡ E )

Syntax hints:   = wceq 1570   E cep 5560   × cxp 5659  ^◡ccnv 5660   / cqs 8689  Rcnr 10845  ℂcc 11093

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-sep 5257  ax-pr 5404

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-ne 2959  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4488  df-sn 4590  df-pr 4592  df-op 4596  df-br 5110  df-opab 5174  df-eprel 5561  df-xp 5667  df-cnv 5669  df-dm 5671  df-rn 5672  df-res 5673  df-ima 5674  df-ec 8692  df-qs 8696  df-c 11101

This theorem is referenced by:  axmulcom  11135  axaddass  11136  axmulass  11137  axdistr  11138