Theorem rneq 5272

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 5218	. . 3 ⊢ (𝐴 = 𝐵 → ◡𝐴 = ◡𝐵)
2	1	dmeqd 5248	. 2 ⊢ (𝐴 = 𝐵 → dom ◡𝐴 = dom ◡𝐵)
3		df-rn 5049	. 2 ⊢ ran 𝐴 = dom ◡𝐴
4		df-rn 5049	. 2 ⊢ ran 𝐵 = dom ◡𝐵
5	2, 3, 4	3eqtr4g 2669	1 ⊢ (𝐴 = 𝐵 → ran 𝐴 = ran 𝐵)

Syntax hints:   → wi 4   = wceq 1475  ^◡ccnv 5037  dom cdm 5038  ran crn 5039

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-rab 2905  df-v 3175  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-br 4584  df-opab 4644  df-cnv 5046  df-dm 5048  df-rn 5049

This theorem is referenced by:  rneqi  5273  rneqd  5274  feq1  5939  foeq1  6024  fnrnfv  6152  fconst5  6376  frxp  7174  tz7.44-2  7390  tz7.44-3  7391  ixpsnf1o  7834  ordtypecbv  8305  ordtypelem3  8308  dfac8alem  8735  dfac8a  8736  dfac5lem3  8831  dfac9  8841  dfac12lem1  8848  dfac12r  8851  ackbij2  8948  isfin3ds  9034  fin23lem17  9043  fin23lem29  9046  fin23lem30  9047  fin23lem32  9049  fin23lem34  9051  fin23lem35  9052  fin23lem39  9055  fin23lem41  9057  isf33lem  9071  isf34lem6  9085  dcomex  9152  axdc2lem  9153  zorn2lem1  9201  zorn2g  9208  ttukey2g  9221  gruurn  9499  rpnnen1lem6  11695  rpnnen1OLD  11701  relexp0g  13610  relexpsucnnr  13613  dfrtrcl2  13650  mpfrcl  19339  ply1frcl  19504  pnrmopn  20957  isi1f  23247  itg1val  23256  axlowdimlem13  25634  axlowdim1  25639  iscusgra  25985  isuvtx  26016  wwlk  26209  clwwlk  26294  rusgra0edg  26482  isfrgra  26517  ex-rn  26689  gidval  26750  grpoinvfval  26760  grpodivfval  26772  isablo  26784  vciOLD  26800  isvclem  26816  isnvlem  26849  isphg  27056  pj11i  27954  hmopidmch  28396  hmopidmpj  28397  pjss1coi  28406  padct  28885  locfinreflem  29235  locfinref  29236  issibf  29722  sitgfval  29730  mrsubvrs  30673  rdgprc0  30943  rdgprc  30944  dfrdg2  30945  brrangeg  31213  poimirlem24  32603  volsupnfl  32624  elghomlem1OLD  32854  isdivrngo  32919  iscom2  32964  dnnumch1  36632  aomclem3  36644  aomclem8  36649  rclexi  36941  rtrclex  36943  rtrclexi  36947  cnvrcl0  36951  dfrtrcl5  36955  dfrcl2  36985  csbima12gALTVD  38155  unirnmap  38395  ssmapsn  38403  sge0val  39259  vonvolmbl  39551  ausgrusgri  40398  0uhgrsubgr  40503  cusgrsize  40670