Theorem rneq 5931

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 5864	. . 3 ⊢ (𝐴 = 𝐵 → ◡𝐴 = ◡𝐵)
2	1	dmeqd 5900	. 2 ⊢ (𝐴 = 𝐵 → dom ◡𝐴 = dom ◡𝐵)
3		df-rn 5677	. 2 ⊢ ran 𝐴 = dom ◡𝐴
4		df-rn 5677	. 2 ⊢ ran 𝐵 = dom ◡𝐵
5	2, 3, 4	3eqtr4g 2826	1 ⊢ (𝐴 = 𝐵 → ran 𝐴 = ran 𝐵)

This proof depends on syntax axioms:   → wi 4   = wceq 1570  ^◡ccnv 5665  dom cdm 5666  ran crn 5667

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 2148  ax-9 2156  ax-ext 2738

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 2745  df-cleq 2758  df-clel 2841  df-rab 3420  df-v 3460  df-dif 3911  df-un 3913  df-ss 3925  df-nul 4290  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-br 5115  df-opab 5179  df-cnv 5674  df-dm 5676  df-rn 5677

This theorem is used by:  rneqi  5932  rneqd  5933  feq1  6690  foeq1  6795  fnrnfv  6947  fconst5  7211  frxp  8131  tz7.44-2  8403  tz7.44-3  8404  ixpsnf1o  8945  ordtypecbv  9489  ordtypelem3  9492  dfac8alem  10032  dfac8a  10033  dfac5lem3  10128  dfac9  10139  dfac12lem1  10146  dfac12r  10149  ackbij2  10244  isfin3ds  10331  fin23lem17  10340  fin23lem29  10343  fin23lem30  10344  fin23lem32  10346  fin23lem34  10348  fin23lem35  10349  fin23lem39  10352  fin23lem41  10354  isf33lem  10368  isf34lem6  10382  dcomex  10449  axdc2lem  10450  zorn2lem1  10498  zorn2g  10505  ttukey2g  10518  gruurn  10801  rpnnen1lem6  13024  relexp0g  15085  relexpsucnnr  15088  dfrtrcl2  15125  mpfrcl  22273  selvval  22308  ply1frcl  22515  pnrmopn  23537  isi1f  25870  itg1val  25879  madeval  28062  axlowdimlem13  29341  axlowdim1  29346  ausgrusgri  29555  0uhgrsubgr  29666  cusgrsize  29841  ex-rn  30828  gidval  30901  grpoinvfval  30911  grpodivfval  30923  isablo  30935  vciOLD  30950  isvclem  30966  isnvlem  30999  isphg  31206  pj11i  32100  hmopidmch  32542  hmopidmpj  32543  pjss1coi  32552  padct  33100  tocyc01  33469  tocyccntz  33495  unitprodclb  33733  esplyfvaln  33995  esplyind  33996  locfinreflem  34261  locfinref  34262  issibf  34755  sitgfval  34763  onvf1odlem3  35613  mrsubvrs  36035  rdgprc0  36304  rdgprc  36305  dfrdg2  36306  brrangeg  36447  poimirlem24  38336  volsupnfl  38357  elghomlem1OLD  38577  isdivrngo  38642  iscom2  38687  elrefrels2  39288  elrefrels3  39289  refreleq  39291  elcnvrefrels2  39304  elcnvrefrels3  39305  dnnumch1  43812  aomclem3  43824  aomclem8  43829  rclexi  44382  rtrclex  44384  rtrclexi  44388  cnvrcl0  44392  dfrtrcl5  44396  dfrcl2  44441  csbima12gALTVD  45646  modelaxreplem1  45728  modelaxreplem2  45729  modelaxrep  45731  unirnmap  45965  ssmapsn  45973  sge0val  47121  vonvolmbl  47416