Theorem dfcnqs 11139

Description: Technical trick to permit reuse of previous lemmas to prove arithmetic operation laws in ℂ from those in R. The trick involves qsid 8779, 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 11118), 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 11118	. 2 ⊢ ℂ = (R × R)
2		qsid 8779	. 2 ⊢ ((R × R) / ◡ E ) = (R × R)
3	1, 2	eqtr4i 2761	1 ⊢ ℂ = ((R × R) / ◡ E )

Syntax hints:   = wceq 1539   E cep 5578   × cxp 5673  ^◡ccnv 5674   / cqs 8704  Rcnr 10862  ℂcc 11110

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701  ax-sep 5298  ax-nul 5305  ax-pr 5426

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-ne 2939  df-ral 3060  df-rex 3069  df-rab 3431  df-v 3474  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-sn 4628  df-pr 4630  df-op 4634  df-br 5148  df-opab 5210  df-eprel 5579  df-xp 5681  df-cnv 5683  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-ec 8707  df-qs 8711  df-c 11118

This theorem is referenced by:  axmulcom  11152  axaddass  11153  axmulass  11154  axdistr  11155