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

Theorem rneqd 5323
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 5321 . 2 (𝐴 = 𝐵 → ran 𝐴 = ran 𝐵)
31, 2syl 17 1 (𝜑 → ran 𝐴 = ran 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1480  ran crn 5085
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-rab 2917  df-v 3192  df-dif 3563  df-un 3565  df-in 3567  df-ss 3574  df-nul 3898  df-if 4065  df-sn 4156  df-pr 4158  df-op 4162  df-br 4624  df-opab 4684  df-cnv 5092  df-dm 5094  df-rn 5095
This theorem is referenced by:  resima2  5401  resima2OLD  5402  imaeq1  5430  imaeq2  5431  resiima  5449  rnxpid  5536  xpima  5545  funimacnv  5938  fnima  5977  elxp4  7072  elxp5  7073  2ndval  7131  fo2nd  7149  f2ndres  7151  curry1  7229  curry2  7232  oarec  7602  en1  7983  xpassen  8014  xpdom2  8015  sbthlem4  8033  fodomr  8071  dffi3  8297  marypha2lem4  8304  ordtypelem9  8391  dfac12lem1  8925  dfac12r  8928  fin23lem32  9126  fin23lem34  9128  fin23lem35  9129  fin23lem36  9130  fin23lem38  9131  fin23lem39  9132  fin23lem41  9134  itunitc  9203  ttukeylem3  9293  fpwwe2lem6  9417  fpwwe2lem9  9420  wunex2  9520  wuncval2  9529  gruima  9584  rpnnen1lem6  11779  rpnnen1OLD  11785  hashf1lem1  13193  s1rn  13334  relexprng  13736  relexpfld  13739  limsupval  14155  vdwapfval  15618  vdwapval  15620  vdwmc  15625  vdwpc  15627  vdwlem6  15633  vdwlem8  15635  restval  16027  restid2  16031  prdsval  16055  prdsdsval  16078  prdsdsval2  16084  prdsdsval3  16085  imasval  16111  imasdsval  16115  isfull  16510  arwval  16633  gsumvalx  17210  conjsubg  17632  pmtrfrn  17818  psgnfval  17860  sylow1lem2  17954  sylow1lem4  17956  sylow1  17958  sylow2blem1  17975  sylow2b  17978  sylow3lem1  17982  sylow3lem2  17983  sylow3lem3  17984  sylow3lem5  17986  sylow3lem6  17987  sylow3  17988  lsmfval  17993  lsmvalx  17994  oppglsm  17997  subglsm  18026  lsmpropd  18030  efgval2  18077  efgi2  18078  efgtlen  18079  efgsdm  18083  efgsdmi  18085  efgsrel  18087  efgs1b  18089  efgsp1  18090  efgsres  18091  efgsfo  18092  efgrelexlemb  18103  frgpnabllem1  18216  iscyg  18221  iscyggen  18222  gsumxp  18315  dprdval  18342  ablfac2  18428  evlseu  19456  zncyg  19837  cygznlem2a  19856  frlmsplit2  20052  tgrest  20903  ordtval  20933  ordtbas2  20935  ordtcnv  20945  ordtrest  20946  ordtrest2  20948  ispnrm  21083  cmpfi  21151  txval  21307  xkoval  21330  ptval2  21344  ptpjopn  21355  xkoccn  21362  xkoptsub  21397  xkopt  21398  fmval  21687  fmf  21689  txflf  21750  cnextf  21810  subgntr  21850  opnsubg  21851  clsnsg  21853  snclseqg  21859  tsmsval2  21873  tsmsxplem1  21896  ustuqtoplem  21983  utopsnneiplem  21991  utopsnneip  21992  fmucndlem  22035  ressprdsds  22116  mopnval  22183  metuval  22294  metdsval  22590  lebnumlem1  22700  lebnumlem3  22702  pi1xfrcnvlem  22796  pi1xfrcnv  22797  minveclem3b  23139  elovolmr  23184  ovolctb  23198  ovoliunlem3  23212  ovolshftlem1  23217  voliunlem3  23260  voliun  23262  volsup  23264  uniioombllem2  23291  uniioombllem3  23293  mbflimsup  23373  itg1climres  23421  itg2monolem1  23457  itg2i1fseq  23462  itg2cnlem1  23468  ellimc2  23581  dvivth  23711  dvne0  23712  lhop2  23716  lhop  23717  mdegfval  23760  dchrptlem2  24924  dchrpt  24926  tglnunirn  25377  tgisline  25456  perpln1  25539  perpln2  25540  isperp  25541  ishpg  25585  lmif  25611  islmib  25613  edgval  25875  edgopval  25876  edgstruct  25878  edgiedgb  25879  edg0iedg0  25880  uhgr2edg  26027  usgr1e  26064  cplgrop  26254  cusgrexi  26260  structtocusgr  26263  1loopgredg  26317  1egrvtxdg0  26327  umgr2v2eedg  26340  ex-ima  27187  bafval  27347  pj3i  28955  ofrn2  29325  ffsrn  29388  smatrcl  29686  ordtprsval  29788  ordtprsuni  29789  ordtcnvNEW  29790  ordtrestNEW  29791  ordtrest2NEW  29793  qqhval  29842  qqhval2  29850  esumval  29931  esumsnf  29949  esumrnmpt2  29953  esumfsupre  29956  esumsup  29974  sxval  30076  omsval  30178  omsfval  30179  carsggect  30203  sibf0  30219  sitgfval  30226  cvmlift3lem6  31067  mvtval  31158  mvrsval  31163  mrsubrn  31171  mrsub0  31174  mrsubf  31175  mrsubccat  31176  mrsubcn  31177  mrsubco  31179  mrsubvrs  31180  elmsubrn  31186  msubrn  31187  msubf  31190  mstaval  31202  msubvrs  31218  mclsval  31221  trpredeq1  31474  trpredeq2  31475  trpredeq3  31476  filnetlem4  32071  mptsnunlem  32856  dissneqlem  32858  poimirlem3  33083  poimirlem9  33089  poimirlem16  33096  poimirlem17  33097  poimirlem19  33099  poimirlem20  33100  poimirlem24  33104  poimirlem30  33110  poimirlem32  33112  mblfinlem2  33118  ovoliunnfl  33122  voliunnfl  33124  isrngo  33367  drngoi  33421  rngohomval  33434  rngoisoval  33447  idlval  33483  pridlval  33503  maxidlval  33509  igenval  33531  lsatset  33796  docaffvalN  35929  docafvalN  35930  mzpmfp  36829  eldiophb  36839  diophrw  36841  conrel1d  37475  iunrelexp0  37514  rntrclfv  37544  clsneibex  37921  neicvgbex  37931  csbima12gALTOLD  38579  rnsnf  38879  fsneqrn  38912  mptima2  38967  limsupval3  39360  limsupresre  39364  limsupresico  39368  limsuppnfdlem  39369  limsupvaluz  39376  limsupvaluzmpt  39385  limsupvaluz2  39406  supcnvlimsup  39408  supcnvlimsupmpt  39409  fourierdlem60  39720  fourierdlem61  39721  sge0val  39920  sge0z  39929  sge0revalmpt  39932  sge0tsms  39934  sge0sup  39945  sge0split  39963  sge0fodjrnlem  39970  sge0seq  40000  meadjiunlem  40019  meaiuninclem  40034  omeiunle  40068  ovolval2lem  40194  ovolval4lem2  40201  ovolval5lem2  40204  ovolval5lem3  40205  ovolval5  40206  ovnovollem2  40208  smfsuplem2  40355  smfsup  40357  smfsupmpt  40358  smfinf  40361  smfinfmpt  40362  smflimsuplem1  40363  smflimsuplem2  40364  smflimsuplem4  40366  smflimsuplem5  40367  smflimsuplem7  40369  smflimsup  40371  fnrnafv  40576
  Copyright terms: Public domain W3C validator