Theorem rneq 5921

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 5858	. . 3 ⊢ (𝐴 = 𝐵 → ◡𝐴 = ◡𝐵)
2	1	dmeqd 5890	. 2 ⊢ (𝐴 = 𝐵 → dom ◡𝐴 = dom ◡𝐵)
3		df-rn 5670	. 2 ⊢ ran 𝐴 = dom ◡𝐴
4		df-rn 5670	. 2 ⊢ ran 𝐵 = dom ◡𝐵
5	2, 3, 4	3eqtr4g 2796	1 ⊢ (𝐴 = 𝐵 → ran 𝐴 = ran 𝐵)

Syntax hints:   → wi 4   = wceq 1540  ^◡ccnv 5658  dom cdm 5659  ran crn 5660

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 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2715  df-cleq 2728  df-clel 2810  df-rab 3421  df-v 3466  df-dif 3934  df-un 3936  df-ss 3948  df-nul 4314  df-if 4506  df-sn 4607  df-pr 4609  df-op 4613  df-br 5125  df-opab 5187  df-cnv 5667  df-dm 5669  df-rn 5670

This theorem is referenced by:  rneqi  5922  rneqd  5923  feq1  6691  foeq1  6791  fnrnfv  6943  fconst5  7203  frxp  8130  tz7.44-2  8426  tz7.44-3  8427  ixpsnf1o  8957  ordtypecbv  9536  ordtypelem3  9539  dfac8alem  10048  dfac8a  10049  dfac5lem3  10144  dfac9  10156  dfac12lem1  10163  dfac12r  10166  ackbij2  10261  isfin3ds  10348  fin23lem17  10357  fin23lem29  10360  fin23lem30  10361  fin23lem32  10363  fin23lem34  10365  fin23lem35  10366  fin23lem39  10369  fin23lem41  10371  isf33lem  10385  isf34lem6  10399  dcomex  10466  axdc2lem  10467  zorn2lem1  10515  zorn2g  10522  ttukey2g  10535  gruurn  10817  rpnnen1lem6  13003  relexp0g  15046  relexpsucnnr  15049  dfrtrcl2  15086  mpfrcl  22048  selvval  22078  ply1frcl  22261  pnrmopn  23286  isi1f  25632  itg1val  25641  madeval  27817  axlowdimlem13  28938  axlowdim1  28943  ausgrusgri  29152  0uhgrsubgr  29263  cusgrsize  29439  ex-rn  30426  gidval  30498  grpoinvfval  30508  grpodivfval  30520  isablo  30532  vciOLD  30547  isvclem  30563  isnvlem  30596  isphg  30803  pj11i  31697  hmopidmch  32139  hmopidmpj  32140  pjss1coi  32149  padct  32702  tocyc01  33134  tocyccntz  33160  unitprodclb  33409  locfinreflem  33876  locfinref  33877  issibf  34370  sitgfval  34378  mrsubvrs  35549  rdgprc0  35816  rdgprc  35817  dfrdg2  35818  brrangeg  35959  poimirlem24  37673  volsupnfl  37694  elghomlem1OLD  37914  isdivrngo  37979  iscom2  38024  elrefrels2  38541  elrefrels3  38542  refreleq  38544  elcnvrefrels2  38557  elcnvrefrels3  38558  dnnumch1  43035  aomclem3  43047  aomclem8  43052  rclexi  43606  rtrclex  43608  rtrclexi  43612  cnvrcl0  43616  dfrtrcl5  43620  dfrcl2  43665  csbima12gALTVD  44888  modelaxreplem1  44970  modelaxreplem2  44971  modelaxrep  44973  unirnmap  45199  ssmapsn  45207  sge0val  46362  vonvolmbl  46657