Theorem rneqd 5936

Description: Equality deduction for range. (Contributed by NM, 4-Mar-2004.)

Hypothesis

Ref	Expression
rneqd.1	⊢ (𝜑 → 𝐴 = 𝐵)

Assertion

Ref	Expression
rneqd	⊢ (𝜑 → ran 𝐴 = ran 𝐵)

Proof of Theorem rneqd

Step	Hyp	Ref	Expression
1		rneqd.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		rneq 5934	. 2 ⊢ (𝐴 = 𝐵 → ran 𝐴 = ran 𝐵)
3	1, 2	syl 17	1 ⊢ (𝜑 → ran 𝐴 = ran 𝐵)

Syntax hints:   → wi 4   = wceq 1542  ran crn 5677

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 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3434  df-v 3477  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-br 5149  df-opab 5211  df-cnv 5684  df-dm 5686  df-rn 5687

This theorem is referenced by:  resima2  6015  imaeq1  6053  imaeq2  6054  resiima  6073  rnxpid  6170  xpima  6179  funimacnv  6627  fnima  6678  focofo  6816  rnfvprc  6883  elxp4  7910  elxp5  7911  2ndval  7975  fo2nd  7993  f2ndres  7997  curry1  8087  curry2  8090  oarec  8559  en1  9018  en1OLD  9019  xpassen  9063  xpdom2  9064  sbthlem4  9083  fodomr  9125  dffi3  9423  marypha2lem4  9430  ordtypelem9  9518  dfac12lem1  10135  dfac12r  10138  fin23lem32  10336  fin23lem34  10338  fin23lem35  10339  fin23lem36  10340  fin23lem38  10341  fin23lem39  10342  fin23lem41  10344  itunitc  10413  ttukeylem3  10503  fpwwe2lem5  10627  fpwwe2lem8  10630  wunex2  10730  wuncval2  10739  gruima  10794  rpnnen1lem6  12963  hashf1lem1  14412  hashf1lem1OLD  14413  s1rn  14546  relexprng  14990  relexprnd  14992  relexpfld  14993  limsupval  15415  vdwapfval  16901  vdwapval  16903  vdwmc  16908  vdwpc  16910  vdwlem6  16916  vdwlem8  16918  restval  17369  restid2  17373  prdsval  17398  prdsdsval  17421  prdsdsval2  17427  prdsdsval3  17428  imasval  17454  imasdsval  17458  isfull  17858  arwval  17990  gsumvalx  18592  conjsubg  19119  psgnfval  19363  sylow1lem2  19462  sylow1lem4  19464  sylow1  19466  sylow2blem1  19483  sylow2b  19486  sylow3lem1  19490  sylow3lem2  19491  sylow3lem3  19492  sylow3lem5  19494  sylow3lem6  19495  sylow3  19496  lsmfval  19501  lsmvalx  19502  oppglsm  19505  subglsm  19536  lsmpropd  19540  efgval2  19587  efgi2  19588  efgtlen  19589  efgsdm  19593  efgsdmi  19595  efgsrel  19597  efgs1b  19599  efgsp1  19600  efgsres  19601  efgsfo  19602  efgrelexlemb  19613  frgpnabllem1  19736  iscyg  19742  iscyggen  19743  gsumxp  19839  dprdval  19868  ablfac2  19954  rnrhmsubrg  20390  zncyg  21096  cygznlem2a  21115  frlmsplit2  21320  evlseu  21638  tgrest  22655  ordtval  22685  ordtbas2  22687  ordtcnv  22697  ordtrest  22698  ordtrest2  22700  ispnrm  22835  cmpfi  22904  txval  23060  xkoval  23083  ptval2  23097  ptpjopn  23108  xkoccn  23115  xkoptsub  23150  xkopt  23151  fmval  23439  fmf  23441  txflf  23502  cnextf  23562  subgntr  23603  opnsubg  23604  clsnsg  23606  snclseqg  23612  tsmsval2  23626  tsmsxplem1  23649  ustuqtoplem  23736  utopsnneiplem  23744  utopsnneip  23745  fmucndlem  23788  ressprdsds  23869  mopnval  23936  metuval  24050  metdsval  24355  lebnumlem1  24469  lebnumlem3  24471  pi1xfrcnvlem  24564  pi1xfrcnv  24565  minveclem3b  24937  elovolmr  24985  ovolctb  24999  ovoliunlem3  25013  ovolshftlem1  25018  voliunlem3  25061  voliun  25063  volsup  25065  uniioombllem2  25092  uniioombllem3  25094  mbflimsup  25175  itg1climres  25224  itg2monolem1  25260  itg2i1fseq  25265  itg2cnlem1  25271  ellimc2  25386  dvivth  25519  dvne0  25520  lhop2  25524  lhop  25525  mdegfval  25572  dchrptlem2  26758  dchrpt  26760  tglnunirn  27789  tgisline  27868  perpln1  27951  perpln2  27952  isperp  27953  ishpg  28000  lmif  28026  islmib  28028  edgval  28299  edgopval  28301  edgstruct  28303  uhgr2edg  28455  usgr1e  28492  cplgrop  28684  cusgrexi  28690  structtocusgr  28693  1loopgredg  28748  1egrvtxdg0  28758  umgr2v2eedg  28771  ex-ima  29685  bafval  29845  pj3i  31449  elimampt  31850  ofrn2  31853  ffsrn  31942  pfxrn2  32094  pfxrn3  32095  swrdrn2  32106  swrdrn3  32107  gsumzresunsn  32194  gsumhashmul  32196  tocycfv  32256  tocycf  32264  trsp2cyc  32270  cycpmco2f1  32271  cycpmco2rn  32272  cycpmconjvlem  32288  cycpmconjslem2  32302  qusbas2  32506  qusima  32508  qusrn  32509  nsgmgc  32512  nsgqusf1olem2  32514  idlsrgval  32606  algextdeglem1  32761  smatrcl  32765  ordtprsval  32887  ordtprsuni  32888  ordtcnvNEW  32889  ordtrestNEW  32890  ordtrest2NEW  32892  qqhval  32943  qqhval2  32951  prodindf  33010  esumval  33033  esumsnf  33051  esumrnmpt2  33055  esumfsupre  33058  esumsup  33076  sxval  33177  omsval  33281  omsfval  33282  carsggect  33306  sibf0  33322  sitgfval  33329  cvmlift3lem6  34304  satfrnmapom  34350  mvtval  34480  mvrsval  34485  mrsubvrs  34502  elmsubrn  34508  msubrn  34509  mstaval  34524  msubvrs  34540  mclsval  34543  filnetlem4  35255  mptsnunlem  36208  dissneqlem  36210  exrecfnlem  36249  ctbssinf  36276  poimirlem3  36480  poimirlem9  36486  poimirlem16  36493  poimirlem17  36494  poimirlem19  36496  poimirlem20  36497  poimirlem24  36501  poimirlem30  36507  poimirlem32  36509  mblfinlem2  36515  ovoliunnfl  36519  voliunnfl  36521  isrngo  36754  drngoi  36808  rngohomval  36821  rngoisoval  36834  idlval  36870  pridlval  36890  maxidlval  36896  igenval  36918  cnvref4  37208  symrelim  37418  unidmqs  37513  lsatset  37849  docaffvalN  39981  docafvalN  39982  sticksstones2  40952  sticksstones3  40953  qsalrel  41060  prjcrvfval  41370  mzpmfp  41471  eldiophb  41481  diophrw  41483  tfsconcatrn  42078  rp-tfslim  42089  conrel1d  42400  iunrelexp0  42439  rntrclfv  42469  clsneibex  42839  neicvgbex  42849  rnsnf  43867  fsneqrn  43896  mptima2  43936  limsupval3  44395  limsupresre  44399  limsupresico  44403  limsuppnfdlem  44404  limsupvaluz  44411  limsupvaluzmpt  44420  limsupvaluz2  44441  supcnvlimsup  44443  supcnvlimsupmpt  44444  liminfval  44462  liminfval5  44468  limsupresxr  44469  liminfresxr  44470  liminfresico  44474  liminfvalxr  44486  fourierdlem60  44869  fourierdlem61  44870  sge0val  45069  sge0z  45078  sge0revalmpt  45081  sge0tsms  45083  sge0sup  45094  sge0split  45112  sge0fodjrnlem  45119  sge0seq  45149  meadjiunlem  45168  meaiuninclem  45183  omeiunle  45220  ovolval2lem  45346  ovolval4lem2  45353  ovolval5lem2  45356  ovolval5lem3  45357  ovolval5  45358  ovnovollem2  45360  smfsuplem2  45515  smfsup  45517  smfsupmpt  45518  smfinf  45521  smfinfmpt  45522  smflimsuplem1  45523  smflimsuplem2  45524  smflimsuplem4  45526  smflimsuplem5  45527  smflimsuplem7  45529  smflimsup  45531  fnrnafv  45857  afv2eq12d  45910