Theorem rneq 5947

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 5884	. . 3 ⊢ (𝐴 = 𝐵 → ◡𝐴 = ◡𝐵)
2	1	dmeqd 5916	. 2 ⊢ (𝐴 = 𝐵 → dom ◡𝐴 = dom ◡𝐵)
3		df-rn 5696	. 2 ⊢ ran 𝐴 = dom ◡𝐴
4		df-rn 5696	. 2 ⊢ ran 𝐵 = dom ◡𝐵
5	2, 3, 4	3eqtr4g 2802	1 ⊢ (𝐴 = 𝐵 → ran 𝐴 = ran 𝐵)

Syntax hints:   → wi 4   = wceq 1540  ^◡ccnv 5684  dom cdm 5685  ran crn 5686

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-br 5144  df-opab 5206  df-cnv 5693  df-dm 5695  df-rn 5696

This theorem is referenced by:  rneqi  5948  rneqd  5949  feq1  6716  foeq1  6816  fnrnfv  6968  fconst5  7226  frxp  8151  tz7.44-2  8447  tz7.44-3  8448  ixpsnf1o  8978  ordtypecbv  9557  ordtypelem3  9560  dfac8alem  10069  dfac8a  10070  dfac5lem3  10165  dfac9  10177  dfac12lem1  10184  dfac12r  10187  ackbij2  10282  isfin3ds  10369  fin23lem17  10378  fin23lem29  10381  fin23lem30  10382  fin23lem32  10384  fin23lem34  10386  fin23lem35  10387  fin23lem39  10390  fin23lem41  10392  isf33lem  10406  isf34lem6  10420  dcomex  10487  axdc2lem  10488  zorn2lem1  10536  zorn2g  10543  ttukey2g  10556  gruurn  10838  rpnnen1lem6  13024  relexp0g  15061  relexpsucnnr  15064  dfrtrcl2  15101  mpfrcl  22109  selvval  22139  ply1frcl  22322  pnrmopn  23351  isi1f  25709  itg1val  25718  madeval  27891  axlowdimlem13  28969  axlowdim1  28974  ausgrusgri  29185  0uhgrsubgr  29296  cusgrsize  29472  ex-rn  30459  gidval  30531  grpoinvfval  30541  grpodivfval  30553  isablo  30565  vciOLD  30580  isvclem  30596  isnvlem  30629  isphg  30836  pj11i  31730  hmopidmch  32172  hmopidmpj  32173  pjss1coi  32182  padct  32731  tocyc01  33138  tocyccntz  33164  unitprodclb  33417  locfinreflem  33839  locfinref  33840  issibf  34335  sitgfval  34343  mrsubvrs  35527  rdgprc0  35794  rdgprc  35795  dfrdg2  35796  brrangeg  35937  poimirlem24  37651  volsupnfl  37672  elghomlem1OLD  37892  isdivrngo  37957  iscom2  38002  elrefrels2  38519  elrefrels3  38520  refreleq  38522  elcnvrefrels2  38535  elcnvrefrels3  38536  dnnumch1  43056  aomclem3  43068  aomclem8  43073  rclexi  43628  rtrclex  43630  rtrclexi  43634  cnvrcl0  43638  dfrtrcl5  43642  dfrcl2  43687  csbima12gALTVD  44917  modelaxreplem1  44995  modelaxreplem2  44996  modelaxrep  44998  unirnmap  45213  ssmapsn  45221  sge0val  46381  vonvolmbl  46676