MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  rneqd Structured version   Visualization version   GIF version

Theorem rneqd 5258
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
StepHypRef Expression
1 rneqd.1 . 2 (𝜑𝐴 = 𝐵)
2 rneq 5256 . 2 (𝐴 = 𝐵 → ran 𝐴 = ran 𝐵)
31, 2syl 17 1 (𝜑 → ran 𝐴 = ran 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1474  ran crn 5026
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2032  ax-13 2229  ax-ext 2586
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2593  df-cleq 2599  df-clel 2602  df-nfc 2736  df-rab 2901  df-v 3171  df-dif 3539  df-un 3541  df-in 3543  df-ss 3550  df-nul 3871  df-if 4033  df-sn 4122  df-pr 4124  df-op 4128  df-br 4575  df-opab 4635  df-cnv 5033  df-dm 5035  df-rn 5036
This theorem is referenced by:  resima2  5336  resima2OLD  5337  imaeq1  5364  imaeq2  5365  resiima  5383  rnxpid  5469  xpima  5478  funimacnv  5867  fnima  5906  elxp4  6977  elxp5  6978  2ndval  7036  fo2nd  7054  f2ndres  7056  curry1  7130  curry2  7133  oarec  7503  en1  7883  xpassen  7913  xpdom2  7914  sbthlem4  7932  fodomr  7970  dffi3  8194  marypha2lem4  8201  ordtypelem9  8288  dfac12lem1  8822  dfac12r  8825  fin23lem32  9023  fin23lem34  9025  fin23lem35  9026  fin23lem36  9027  fin23lem38  9028  fin23lem39  9029  fin23lem41  9031  itunitc  9100  ttukeylem3  9190  fpwwe2lem6  9310  fpwwe2lem9  9313  wunex2  9413  wuncval2  9422  gruima  9477  rpnnen1lem6  11648  rpnnen1OLD  11654  hashf1lem1  13045  s1rn  13175  relexprng  13577  relexpfld  13580  limsupval  13996  vdwapfval  15456  vdwapval  15458  vdwmc  15463  vdwpc  15465  vdwlem6  15471  vdwlem8  15473  restval  15853  restid2  15857  prdsval  15881  prdsdsval  15904  prdsdsval2  15910  prdsdsval3  15911  imasval  15937  imasdsval  15941  isfull  16336  arwval  16459  gsumvalx  17036  conjsubg  17458  pmtrfrn  17644  psgnfval  17686  sylow1lem2  17780  sylow1lem4  17782  sylow1  17784  sylow2blem1  17801  sylow2b  17804  sylow3lem1  17808  sylow3lem2  17809  sylow3lem3  17810  sylow3lem5  17812  sylow3lem6  17813  sylow3  17814  lsmfval  17819  lsmvalx  17820  oppglsm  17823  subglsm  17852  lsmpropd  17856  efgval2  17903  efgi2  17904  efgtlen  17905  efgsdm  17909  efgsdmi  17911  efgsrel  17913  efgs1b  17915  efgsp1  17916  efgsres  17917  efgsfo  17918  efgrelexlemb  17929  frgpnabllem1  18042  iscyg  18047  iscyggen  18048  gsumxp  18141  dprdval  18168  ablfac2  18254  evlseu  19280  zncyg  19658  cygznlem2a  19677  frlmsplit2  19870  tgrest  20712  ordtval  20742  ordtbas2  20744  ordtcnv  20754  ordtrest  20755  ordtrest2  20757  ispnrm  20892  cmpfi  20960  txval  21116  xkoval  21139  ptval2  21153  ptpjopn  21164  xkoccn  21171  xkoptsub  21206  xkopt  21207  fmval  21496  fmf  21498  txflf  21559  cnextf  21619  subgntr  21659  opnsubg  21660  clsnsg  21662  snclseqg  21668  tsmsval2  21682  tsmsxplem1  21705  ustuqtoplem  21792  utopsnneiplem  21800  utopsnneip  21801  fmucndlem  21844  ressprdsds  21924  mopnval  21991  metuval  22102  metdsval  22386  lebnumlem1  22496  lebnumlem3  22498  pi1xfrcnvlem  22592  pi1xfrcnv  22593  minveclem3b  22921  elovolmr  22965  ovolctb  22979  ovoliunlem3  22993  ovolshftlem1  22998  voliunlem3  23041  voliun  23043  volsup  23045  uniioombllem2  23071  uniioombllem3  23073  mbflimsup  23153  itg1climres  23201  itg2monolem1  23237  itg2i1fseq  23242  itg2cnlem1  23248  ellimc2  23361  dvivth  23491  dvne0  23492  lhop2  23496  lhop  23497  mdegfval  23540  dchrptlem2  24704  dchrpt  24706  tglnunirn  25158  tgisline  25237  perpln1  25320  perpln2  25321  isperp  25322  ishpg  25366  lmif  25392  islmib  25394  edgval  25631  edgopval  25632  edgss  25644  nbgraop  25715  nbgraopALT  25716  ex-ima  26454  vcoprneOLD  26597  bafval  26624  pj3i  28254  ofrn2  28625  ffsrn  28695  smatrcl  28993  ordtprsval  29095  ordtprsuni  29096  ordtcnvNEW  29097  ordtrestNEW  29098  ordtrest2NEW  29100  qqhval  29149  qqhval2  29157  esumval  29238  esumsnf  29256  esumrnmpt2  29260  esumfsupre  29263  esumsup  29281  sxval  29383  omsval  29485  omsfval  29486  carsggect  29510  sibf0  29526  sitgfval  29533  cvmlift3lem6  30363  mvtval  30454  mvrsval  30459  mrsubrn  30467  mrsub0  30470  mrsubf  30471  mrsubccat  30472  mrsubcn  30473  mrsubco  30475  mrsubvrs  30476  elmsubrn  30482  msubrn  30483  msubf  30486  mstaval  30498  msubvrs  30514  mclsval  30517  trpredeq1  30767  trpredeq2  30768  trpredeq3  30769  filnetlem4  31349  mptsnunlem  32161  dissneqlem  32163  poimirlem3  32382  poimirlem9  32388  poimirlem16  32395  poimirlem17  32396  poimirlem19  32398  poimirlem20  32399  poimirlem24  32403  poimirlem30  32409  poimirlem32  32411  mblfinlem2  32417  ovoliunnfl  32421  voliunnfl  32423  isrngo  32666  drngoi  32720  rngohomval  32733  rngoisoval  32746  idlval  32782  pridlval  32802  maxidlval  32808  igenval  32830  lsatset  33095  docaffvalN  35228  docafvalN  35229  mzpmfp  36128  eldiophb  36138  diophrw  36140  conrel1d  36774  iunrelexp0  36813  rntrclfv  36843  clsneibex  37220  neicvgbex  37230  csbima12gALTOLD  37879  rnsnf  38165  fsneqrn  38198  fourierdlem60  38860  fourierdlem61  38861  sge0val  39060  sge0z  39069  sge0revalmpt  39072  sge0tsms  39074  sge0sup  39085  sge0split  39103  sge0fodjrnlem  39110  sge0seq  39140  meadjiunlem  39159  meaiuninclem  39174  omeiunle  39208  ovolval2lem  39334  ovolval4lem2  39341  ovolval5lem2  39344  ovolval5lem3  39345  ovolval5  39346  ovnovollem2  39348  fnrnafv  39693  edgaval  40352  edgaopval  40353  edgastruct  40355  edgiedgb  40356  edg0iedg0  40358  uhgr2edg  40434  usgr1e  40470  cplgrop  40658  cusgrexi  40661  1loopgredg  40715  1egrvtxdg0  40726  umgr2v2eedg  40739
  Copyright terms: Public domain W3C validator