Theorem rneq 5882

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 5820	. . 3 ⊢ (𝐴 = 𝐵 → ◡𝐴 = ◡𝐵)
2	1	dmeqd 5852	. 2 ⊢ (𝐴 = 𝐵 → dom ◡𝐴 = dom ◡𝐵)
3		df-rn 5634	. 2 ⊢ ran 𝐴 = dom ◡𝐴
4		df-rn 5634	. 2 ⊢ ran 𝐵 = dom ◡𝐵
5	2, 3, 4	3eqtr4g 2789	1 ⊢ (𝐴 = 𝐵 → ran 𝐴 = ran 𝐵)

Syntax hints:   → wi 4   = wceq 1540  ^◡ccnv 5622  dom cdm 5623  ran crn 5624

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 2701

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 2708  df-cleq 2721  df-clel 2803  df-rab 3397  df-v 3440  df-dif 3908  df-un 3910  df-ss 3922  df-nul 4287  df-if 4479  df-sn 4580  df-pr 4582  df-op 4586  df-br 5096  df-opab 5158  df-cnv 5631  df-dm 5633  df-rn 5634

This theorem is referenced by:  rneqi  5883  rneqd  5884  feq1  6634  foeq1  6736  fnrnfv  6886  fconst5  7146  frxp  8066  tz7.44-2  8336  tz7.44-3  8337  ixpsnf1o  8872  ordtypecbv  9428  ordtypelem3  9431  dfac8alem  9942  dfac8a  9943  dfac5lem3  10038  dfac9  10050  dfac12lem1  10057  dfac12r  10060  ackbij2  10155  isfin3ds  10242  fin23lem17  10251  fin23lem29  10254  fin23lem30  10255  fin23lem32  10257  fin23lem34  10259  fin23lem35  10260  fin23lem39  10263  fin23lem41  10265  isf33lem  10279  isf34lem6  10293  dcomex  10360  axdc2lem  10361  zorn2lem1  10409  zorn2g  10416  ttukey2g  10429  gruurn  10711  rpnnen1lem6  12901  relexp0g  14947  relexpsucnnr  14950  dfrtrcl2  14987  mpfrcl  22008  selvval  22038  ply1frcl  22221  pnrmopn  23246  isi1f  25591  itg1val  25600  madeval  27780  axlowdimlem13  28917  axlowdim1  28922  ausgrusgri  29131  0uhgrsubgr  29242  cusgrsize  29418  ex-rn  30402  gidval  30474  grpoinvfval  30484  grpodivfval  30496  isablo  30508  vciOLD  30523  isvclem  30539  isnvlem  30572  isphg  30779  pj11i  31673  hmopidmch  32115  hmopidmpj  32116  pjss1coi  32125  padct  32676  tocyc01  33073  tocyccntz  33099  unitprodclb  33339  locfinreflem  33809  locfinref  33810  issibf  34303  sitgfval  34311  onvf1odlem3  35080  mrsubvrs  35497  rdgprc0  35769  rdgprc  35770  dfrdg2  35771  brrangeg  35912  poimirlem24  37626  volsupnfl  37647  elghomlem1OLD  37867  isdivrngo  37932  iscom2  37977  elrefrels2  38497  elrefrels3  38498  refreleq  38500  elcnvrefrels2  38513  elcnvrefrels3  38514  dnnumch1  43020  aomclem3  43032  aomclem8  43037  rclexi  43591  rtrclex  43593  rtrclexi  43597  cnvrcl0  43601  dfrtrcl5  43605  dfrcl2  43650  csbima12gALTVD  44873  modelaxreplem1  44955  modelaxreplem2  44956  modelaxrep  44958  unirnmap  45189  ssmapsn  45197  sge0val  46351  vonvolmbl  46646