Theorem rneq 5845

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 5782	. . 3 ⊢ (𝐴 = 𝐵 → ◡𝐴 = ◡𝐵)
2	1	dmeqd 5814	. 2 ⊢ (𝐴 = 𝐵 → dom ◡𝐴 = dom ◡𝐵)
3		df-rn 5600	. 2 ⊢ ran 𝐴 = dom ◡𝐴
4		df-rn 5600	. 2 ⊢ ran 𝐵 = dom ◡𝐵
5	2, 3, 4	3eqtr4g 2803	1 ⊢ (𝐴 = 𝐵 → ran 𝐴 = ran 𝐵)

Syntax hints:   → wi 4   = wceq 1539  ^◡ccnv 5588  dom cdm 5589  ran crn 5590

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-rab 3073  df-v 3434  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-nul 4257  df-if 4460  df-sn 4562  df-pr 4564  df-op 4568  df-br 5075  df-opab 5137  df-cnv 5597  df-dm 5599  df-rn 5600

This theorem is referenced by:  rneqi  5846  rneqd  5847  feq1  6581  foeq1  6684  fnrnfv  6829  fconst5  7081  frxp  7967  tz7.44-2  8238  tz7.44-3  8239  ixpsnf1o  8726  ordtypecbv  9276  ordtypelem3  9279  dfac8alem  9785  dfac8a  9786  dfac5lem3  9881  dfac9  9892  dfac12lem1  9899  dfac12r  9902  ackbij2  9999  isfin3ds  10085  fin23lem17  10094  fin23lem29  10097  fin23lem30  10098  fin23lem32  10100  fin23lem34  10102  fin23lem35  10103  fin23lem39  10106  fin23lem41  10108  isf33lem  10122  isf34lem6  10136  dcomex  10203  axdc2lem  10204  zorn2lem1  10252  zorn2g  10259  ttukey2g  10272  gruurn  10554  rpnnen1lem6  12722  relexp0g  14733  relexpsucnnr  14736  dfrtrcl2  14773  mpfrcl  21295  selvval  21328  ply1frcl  21484  pnrmopn  22494  isi1f  24838  itg1val  24847  axlowdimlem13  27322  axlowdim1  27327  ausgrusgri  27538  0uhgrsubgr  27646  cusgrsize  27821  ex-rn  28804  gidval  28874  grpoinvfval  28884  grpodivfval  28896  isablo  28908  vciOLD  28923  isvclem  28939  isnvlem  28972  isphg  29179  pj11i  30073  hmopidmch  30515  hmopidmpj  30516  pjss1coi  30525  padct  31054  tocyc01  31385  tocyccntz  31411  locfinreflem  31790  locfinref  31791  issibf  32300  sitgfval  32308  mrsubvrs  33484  rdgprc0  33769  rdgprc  33770  dfrdg2  33771  madeval  34036  brrangeg  34238  poimirlem24  35801  volsupnfl  35822  elghomlem1OLD  36043  isdivrngo  36108  iscom2  36153  elrefrels2  36635  elrefrels3  36636  refreleq  36638  elcnvrefrels2  36648  elcnvrefrels3  36649  dnnumch1  40869  aomclem3  40881  aomclem8  40886  rclexi  41223  rtrclex  41225  rtrclexi  41229  cnvrcl0  41233  dfrtrcl5  41237  dfrcl2  41282  csbima12gALTVD  42517  unirnmap  42748  ssmapsn  42756  sge0val  43904  vonvolmbl  44199