Theorem rneq 5770

Description: Equality theorem for range. (Contributed by NM, 29-Dec-1996.)

Assertion

Ref	Expression
rneq	⊢ (𝐴 = 𝐵 → ran 𝐴 = ran 𝐵)

Proof of Theorem rneq

Step	Hyp	Ref	Expression
1		cnveq 5708	. . 3 ⊢ (𝐴 = 𝐵 → ◡𝐴 = ◡𝐵)
2	1	dmeqd 5738	. 2 ⊢ (𝐴 = 𝐵 → dom ◡𝐴 = dom ◡𝐵)
3		df-rn 5530	. 2 ⊢ ran 𝐴 = dom ◡𝐴
4		df-rn 5530	. 2 ⊢ ran 𝐵 = dom ◡𝐵
5	2, 3, 4	3eqtr4g 2858	1 ⊢ (𝐴 = 𝐵 → ran 𝐴 = ran 𝐵)

Syntax hints:   → wi 4   = wceq 1538  ^◡ccnv 5518  dom cdm 5519  ran crn 5520

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-v 3443  df-un 3886  df-in 3888  df-ss 3898  df-sn 4526  df-pr 4528  df-op 4532  df-br 5031  df-opab 5093  df-cnv 5527  df-dm 5529  df-rn 5530

This theorem is referenced by:  rneqi  5771  rneqd  5772  feq1  6468  foeq1  6561  fnrnfv  6700  fconst5  6945  frxp  7803  tz7.44-2  8026  tz7.44-3  8027  ixpsnf1o  8485  ordtypecbv  8965  ordtypelem3  8968  dfac8alem  9440  dfac8a  9441  dfac5lem3  9536  dfac9  9547  dfac12lem1  9554  dfac12r  9557  ackbij2  9654  isfin3ds  9740  fin23lem17  9749  fin23lem29  9752  fin23lem30  9753  fin23lem32  9755  fin23lem34  9757  fin23lem35  9758  fin23lem39  9761  fin23lem41  9763  isf33lem  9777  isf34lem6  9791  dcomex  9858  axdc2lem  9859  zorn2lem1  9907  zorn2g  9914  ttukey2g  9927  gruurn  10209  rpnnen1lem6  12369  relexp0g  14373  relexpsucnnr  14376  dfrtrcl2  14413  mpfrcl  20757  selvval  20790  ply1frcl  20942  pnrmopn  21948  isi1f  24278  itg1val  24287  axlowdimlem13  26748  axlowdim1  26753  ausgrusgri  26961  0uhgrsubgr  27069  cusgrsize  27244  ex-rn  28225  gidval  28295  grpoinvfval  28305  grpodivfval  28317  isablo  28329  vciOLD  28344  isvclem  28360  isnvlem  28393  isphg  28600  pj11i  29494  hmopidmch  29936  hmopidmpj  29937  pjss1coi  29946  padct  30481  tocyc01  30810  tocyccntz  30836  locfinreflem  31193  locfinref  31194  issibf  31701  sitgfval  31709  mrsubvrs  32882  rdgprc0  33151  rdgprc  33152  dfrdg2  33153  madeval  33402  brrangeg  33510  poimirlem24  35081  volsupnfl  35102  elghomlem1OLD  35323  isdivrngo  35388  iscom2  35433  elrefrels2  35917  elrefrels3  35918  refreleq  35920  elcnvrefrels2  35930  elcnvrefrels3  35931  dnnumch1  39988  aomclem3  40000  aomclem8  40005  rclexi  40315  rtrclex  40317  rtrclexi  40321  cnvrcl0  40325  dfrtrcl5  40329  dfrcl2  40375  csbima12gALTVD  41603  unirnmap  41837  ssmapsn  41845  sge0val  43005  vonvolmbl  43300