Theorem rneq 5924

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570  ^◡ccnv 5658  dom cdm 5659  ran crn 5660

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-rab 3415  df-v 3455  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4283  df-if 4486  df-sn 4588  df-pr 4590  df-op 4594  df-br 5108  df-opab 5172  df-cnv 5667  df-dm 5669  df-rn 5670

This theorem is used by:  rneqi  5925  rneqd  5926  feq1  6684  foeq1  6789  fnrnfv  6941  fconst5  7209  frxp  8128  tz7.44-2  8400  tz7.44-3  8401  ixpsnf1o  8949  ordtypecbv  9493  ordtypelem3  9496  dfac8alem  10036  dfac8a  10037  dfac5lem3  10132  dfac9  10143  dfac12lem1  10150  dfac12r  10153  ackbij2  10248  isfin3ds  10335  fin23lem17  10344  fin23lem29  10347  fin23lem30  10348  fin23lem32  10350  fin23lem34  10352  fin23lem35  10353  fin23lem39  10356  fin23lem41  10358  isf33lem  10372  isf34lem6  10386  dcomex  10453  axdc2lem  10454  zorn2lem1  10502  zorn2g  10509  ttukey2g  10522  gruurn  10811  rpnnen1lem6  13036  relexp0g  15099  relexpsucnnr  15102  dfrtrcl2  15139  mpfrcl  22307  selvval  22342  ply1frcl  22549  pnrmopn  23574  isi1f  25908  itg1val  25917  madeval  28105  axlowdimlem13  29419  axlowdim1  29424  ausgrusgri  29636  0uhgrsubgr  29747  cusgrsize  29922  ex-rn  30928  gidval  31001  grpoinvfval  31011  grpodivfval  31023  isablo  31035  vciOLD  31050  isvclem  31066  isnvlem  31099  isphg  31306  pj11i  32200  hmopidmch  32642  hmopidmpj  32643  pjss1coi  32652  padct  33197  tocyc01  33566  tocyccntz  33592  unitprodclb  33830  esplyfvaln  34092  esplyind  34093  locfinreflem  34358  locfinref  34359  issibf  34852  sitgfval  34860  onvf1odlem3  35710  mrsubvrs  36109  rdgprc0  36378  rdgprc  36379  dfrdg2  36380  brrangeg  36521  poimirlem24  38401  volsupnfl  38422  elghomlem1OLD  38643  isdivrngo  38708  iscom2  38753  elrefrels2  39354  elrefrels3  39355  refreleq  39357  elcnvrefrels2  39370  elcnvrefrels3  39371  dnnumch1  43893  aomclem3  43905  aomclem8  43910  rclexi  44463  rtrclex  44465  rtrclexi  44469  cnvrcl0  44473  dfrtrcl5  44477  dfrcl2  44522  csbima12gALTVD  45727  modelaxreplem1  45809  modelaxreplem2  45810  modelaxrep  45812  unirnmap  46046  ssmapsn  46054  sge0val  47202  vonvolmbl  47497