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

Theorem rneqd 5776
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 5774 . 2 (𝐴 = 𝐵 → ran 𝐴 = ran 𝐵)
31, 2syl 17 1 (𝜑 → ran 𝐴 = ran 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1538  ran crn 5524
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2773
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2780  df-cleq 2794  df-clel 2873  df-nfc 2941  df-v 3446  df-un 3889  df-in 3891  df-ss 3901  df-sn 4529  df-pr 4531  df-op 4535  df-br 5034  df-opab 5096  df-cnv 5531  df-dm 5533  df-rn 5534
This theorem is referenced by:  resima2  5857  imaeq1  5895  imaeq2  5896  resiima  5915  rnxpid  6001  xpima  6010  funimacnv  6409  fnima  6454  rnfvprc  6643  elxp4  7613  elxp5  7614  2ndval  7678  fo2nd  7696  f2ndres  7700  curry1  7786  curry2  7789  oarec  8175  en1  8563  xpassen  8598  xpdom2  8599  sbthlem4  8618  fodomr  8656  dffi3  8883  marypha2lem4  8890  ordtypelem9  8978  dfac12lem1  9558  dfac12r  9561  fin23lem32  9759  fin23lem34  9761  fin23lem35  9762  fin23lem36  9763  fin23lem38  9764  fin23lem39  9765  fin23lem41  9767  itunitc  9836  ttukeylem3  9926  fpwwe2lem6  10050  fpwwe2lem9  10053  wunex2  10153  wuncval2  10162  gruima  10217  rpnnen1lem6  12373  hashf1lem1  13813  s1rn  13948  relexprng  14401  relexprnd  14403  relexpfld  14404  limsupval  14827  vdwapfval  16301  vdwapval  16303  vdwmc  16308  vdwpc  16310  vdwlem6  16316  vdwlem8  16318  restval  16696  restid2  16700  prdsval  16724  prdsdsval  16747  prdsdsval2  16753  prdsdsval3  16754  imasval  16780  imasdsval  16784  isfull  17176  arwval  17299  gsumvalx  17882  conjsubg  18386  psgnfval  18624  sylow1lem2  18720  sylow1lem4  18722  sylow1  18724  sylow2blem1  18741  sylow2b  18744  sylow3lem1  18748  sylow3lem2  18749  sylow3lem3  18750  sylow3lem5  18752  sylow3lem6  18753  sylow3  18754  lsmfval  18759  lsmvalx  18760  oppglsm  18763  subglsm  18795  lsmpropd  18799  efgval2  18846  efgi2  18847  efgtlen  18848  efgsdm  18852  efgsdmi  18854  efgsrel  18856  efgs1b  18858  efgsp1  18859  efgsres  18860  efgsfo  18861  efgrelexlemb  18872  frgpnabllem1  18990  iscyg  18995  iscyggen  18996  gsumxp  19093  dprdval  19122  ablfac2  19208  rnrhmsubrg  19564  zncyg  20244  cygznlem2a  20263  frlmsplit2  20466  evlseu  20759  tgrest  21768  ordtval  21798  ordtbas2  21800  ordtcnv  21810  ordtrest  21811  ordtrest2  21813  ispnrm  21948  cmpfi  22017  txval  22173  xkoval  22196  ptval2  22210  ptpjopn  22221  xkoccn  22228  xkoptsub  22263  xkopt  22264  fmval  22552  fmf  22554  txflf  22615  cnextf  22675  subgntr  22716  opnsubg  22717  clsnsg  22719  snclseqg  22725  tsmsval2  22739  tsmsxplem1  22762  ustuqtoplem  22849  utopsnneiplem  22857  utopsnneip  22858  fmucndlem  22901  ressprdsds  22982  mopnval  23049  metuval  23160  metdsval  23456  lebnumlem1  23570  lebnumlem3  23572  pi1xfrcnvlem  23665  pi1xfrcnv  23666  minveclem3b  24036  elovolmr  24084  ovolctb  24098  ovoliunlem3  24112  ovolshftlem1  24117  voliunlem3  24160  voliun  24162  volsup  24164  uniioombllem2  24191  uniioombllem3  24193  mbflimsup  24274  itg1climres  24322  itg2monolem1  24358  itg2i1fseq  24363  itg2cnlem1  24369  ellimc2  24484  dvivth  24617  dvne0  24618  lhop2  24622  lhop  24623  mdegfval  24667  dchrptlem2  25853  dchrpt  25855  tglnunirn  26346  tgisline  26425  perpln1  26508  perpln2  26509  isperp  26510  ishpg  26557  lmif  26583  islmib  26585  edgval  26846  edgopval  26848  edgstruct  26850  uhgr2edg  27002  usgr1e  27039  cplgrop  27231  cusgrexi  27237  structtocusgr  27240  1loopgredg  27295  1egrvtxdg0  27305  umgr2v2eedg  27318  ex-ima  28231  bafval  28391  pj3i  29995  elimampt  30401  ofrn2  30405  ffsrn  30495  pfxrn2  30646  pfxrn3  30647  swrdrn2  30658  swrdrn3  30659  gsumzresunsn  30743  gsumhashmul  30745  tocycfv  30805  tocycf  30813  trsp2cyc  30819  cycpmco2f1  30820  cycpmco2rn  30821  cycpmconjvlem  30837  cycpmconjslem2  30851  idlsrgval  31060  smatrcl  31153  ordtprsval  31275  ordtprsuni  31276  ordtcnvNEW  31277  ordtrestNEW  31278  ordtrest2NEW  31280  qqhval  31329  qqhval2  31337  prodindf  31396  esumval  31419  esumsnf  31437  esumrnmpt2  31441  esumfsupre  31444  esumsup  31462  sxval  31563  omsval  31665  omsfval  31666  carsggect  31690  sibf0  31706  sitgfval  31713  cvmlift3lem6  32685  satfrnmapom  32731  mvtval  32861  mvrsval  32866  mrsubvrs  32883  elmsubrn  32889  msubrn  32890  mstaval  32905  msubvrs  32921  mclsval  32924  trpredeq1  33173  trpredeq2  33174  trpredeq3  33175  filnetlem4  33843  mptsnunlem  34756  dissneqlem  34758  exrecfnlem  34797  ctbssinf  34824  poimirlem3  35059  poimirlem9  35065  poimirlem16  35072  poimirlem17  35073  poimirlem19  35075  poimirlem20  35076  poimirlem24  35080  poimirlem30  35086  poimirlem32  35088  mblfinlem2  35094  ovoliunnfl  35098  voliunnfl  35100  isrngo  35334  drngoi  35388  rngohomval  35401  rngoisoval  35414  idlval  35450  pridlval  35470  maxidlval  35476  igenval  35498  symrelim  35954  unidmqs  36047  lsatset  36285  docaffvalN  38416  docafvalN  38417  qsalrel  39417  mzpmfp  39685  eldiophb  39695  diophrw  39697  conrel1d  40361  iunrelexp0  40400  rntrclfv  40430  clsneibex  40802  neicvgbex  40812  rnsnf  41807  fsneqrn  41837  mptima2  41880  limsupval3  42331  limsupresre  42335  limsupresico  42339  limsuppnfdlem  42340  limsupvaluz  42347  limsupvaluzmpt  42356  limsupvaluz2  42377  supcnvlimsup  42379  supcnvlimsupmpt  42380  liminfval  42398  liminfval5  42404  limsupresxr  42405  liminfresxr  42406  liminfresico  42410  liminfvalxr  42422  fourierdlem60  42805  fourierdlem61  42806  sge0val  43002  sge0z  43011  sge0revalmpt  43014  sge0tsms  43016  sge0sup  43027  sge0split  43045  sge0fodjrnlem  43052  sge0seq  43082  meadjiunlem  43101  meaiuninclem  43116  omeiunle  43153  ovolval2lem  43279  ovolval4lem2  43286  ovolval5lem2  43289  ovolval5lem3  43290  ovolval5  43291  ovnovollem2  43293  smfsuplem2  43440  smfsup  43442  smfsupmpt  43443  smfinf  43446  smfinfmpt  43447  smflimsuplem1  43448  smflimsuplem2  43449  smflimsuplem4  43451  smflimsuplem5  43452  smflimsuplem7  43454  smflimsup  43456  fnrnafv  43715  afv2eq12d  43768
  Copyright terms: Public domain W3C validator