Theorem rneq 5880

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 5817	. . 3 ⊢ (𝐴 = 𝐵 → ◡𝐴 = ◡𝐵)
2	1	dmeqd 5849	. 2 ⊢ (𝐴 = 𝐵 → dom ◡𝐴 = dom ◡𝐵)
3		df-rn 5630	. 2 ⊢ ran 𝐴 = dom ◡𝐴
4		df-rn 5630	. 2 ⊢ ran 𝐵 = dom ◡𝐵
5	2, 3, 4	3eqtr4g 2793	1 ⊢ (𝐴 = 𝐵 → ran 𝐴 = ran 𝐵)

Syntax hints:   → wi 4   = wceq 1541  ^◡ccnv 5618  dom cdm 5619  ran crn 5620

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-rab 3397  df-v 3439  df-dif 3901  df-un 3903  df-ss 3915  df-nul 4283  df-if 4475  df-sn 4576  df-pr 4578  df-op 4582  df-br 5094  df-opab 5156  df-cnv 5627  df-dm 5629  df-rn 5630

This theorem is referenced by:  rneqi  5881  rneqd  5882  feq1  6634  foeq1  6736  fnrnfv  6887  fconst5  7146  frxp  8062  tz7.44-2  8332  tz7.44-3  8333  ixpsnf1o  8868  ordtypecbv  9410  ordtypelem3  9413  dfac8alem  9927  dfac8a  9928  dfac5lem3  10023  dfac9  10035  dfac12lem1  10042  dfac12r  10045  ackbij2  10140  isfin3ds  10227  fin23lem17  10236  fin23lem29  10239  fin23lem30  10240  fin23lem32  10242  fin23lem34  10244  fin23lem35  10245  fin23lem39  10248  fin23lem41  10250  isf33lem  10264  isf34lem6  10278  dcomex  10345  axdc2lem  10346  zorn2lem1  10394  zorn2g  10401  ttukey2g  10414  gruurn  10696  rpnnen1lem6  12882  relexp0g  14931  relexpsucnnr  14934  dfrtrcl2  14971  mpfrcl  22021  selvval  22051  ply1frcl  22234  pnrmopn  23259  isi1f  25603  itg1val  25612  madeval  27794  axlowdimlem13  28934  axlowdim1  28939  ausgrusgri  29148  0uhgrsubgr  29259  cusgrsize  29435  ex-rn  30422  gidval  30494  grpoinvfval  30504  grpodivfval  30516  isablo  30528  vciOLD  30543  isvclem  30559  isnvlem  30592  isphg  30799  pj11i  31693  hmopidmch  32135  hmopidmpj  32136  pjss1coi  32145  padct  32705  tocyc01  33094  tocyccntz  33120  unitprodclb  33361  esplyind  33613  locfinreflem  33874  locfinref  33875  issibf  34367  sitgfval  34375  onvf1odlem3  35170  mrsubvrs  35587  rdgprc0  35856  rdgprc  35857  dfrdg2  35858  brrangeg  35999  poimirlem24  37705  volsupnfl  37726  elghomlem1OLD  37946  isdivrngo  38011  iscom2  38056  elrefrels2  38631  elrefrels3  38632  refreleq  38634  elcnvrefrels2  38647  elcnvrefrels3  38648  dnnumch1  43162  aomclem3  43174  aomclem8  43179  rclexi  43733  rtrclex  43735  rtrclexi  43739  cnvrcl0  43743  dfrtrcl5  43747  dfrcl2  43792  csbima12gALTVD  45014  modelaxreplem1  45096  modelaxreplem2  45097  modelaxrep  45099  unirnmap  45330  ssmapsn  45338  sge0val  46489  vonvolmbl  46784