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

Theorem rneqd 5802
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 5800 . 2 (𝐴 = 𝐵 → ran 𝐴 = ran 𝐵)
31, 2syl 17 1 (𝜑 → ran 𝐴 = ran 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1528  ran crn 5550
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2793
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-rab 3147  df-v 3497  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-nul 4291  df-if 4466  df-sn 4560  df-pr 4562  df-op 4566  df-br 5059  df-opab 5121  df-cnv 5557  df-dm 5559  df-rn 5560
This theorem is referenced by:  resima2  5882  imaeq1  5918  imaeq2  5919  resiima  5938  rnxpid  6024  xpima  6033  funimacnv  6429  fnima  6472  rnfvprc  6658  elxp4  7615  elxp5  7616  2ndval  7683  fo2nd  7701  f2ndres  7705  curry1  7790  curry2  7793  oarec  8178  en1  8565  xpassen  8600  xpdom2  8601  sbthlem4  8619  fodomr  8657  dffi3  8884  marypha2lem4  8891  ordtypelem9  8979  dfac12lem1  9558  dfac12r  9561  fin23lem32  9755  fin23lem34  9757  fin23lem35  9758  fin23lem36  9759  fin23lem38  9760  fin23lem39  9761  fin23lem41  9763  itunitc  9832  ttukeylem3  9922  fpwwe2lem6  10046  fpwwe2lem9  10049  wunex2  10149  wuncval2  10158  gruima  10213  rpnnen1lem6  12371  hashf1lem1  13803  s1rn  13943  relexprng  14395  relexpfld  14398  limsupval  14821  vdwapfval  16297  vdwapval  16299  vdwmc  16304  vdwpc  16306  vdwlem6  16312  vdwlem8  16314  restval  16690  restid2  16694  prdsval  16718  prdsdsval  16741  prdsdsval2  16747  prdsdsval3  16748  imasval  16774  imasdsval  16778  isfull  17170  arwval  17293  gsumvalx  17876  conjsubg  18330  psgnfval  18559  sylow1lem2  18655  sylow1lem4  18657  sylow1  18659  sylow2blem1  18676  sylow2b  18679  sylow3lem1  18683  sylow3lem2  18684  sylow3lem3  18685  sylow3lem5  18687  sylow3lem6  18688  sylow3  18689  lsmfval  18694  lsmvalx  18695  oppglsm  18698  subglsm  18730  lsmpropd  18734  efgval2  18781  efgi2  18782  efgtlen  18783  efgsdm  18787  efgsdmi  18789  efgsrel  18791  efgs1b  18793  efgsp1  18794  efgsres  18795  efgsfo  18796  efgrelexlemb  18807  frgpnabllem1  18924  iscyg  18929  iscyggen  18930  gsumxp  19027  dprdval  19056  ablfac2  19142  rnrhmsubrg  19498  evlseu  20226  zncyg  20625  cygznlem2a  20644  frlmsplit2  20847  tgrest  21697  ordtval  21727  ordtbas2  21729  ordtcnv  21739  ordtrest  21740  ordtrest2  21742  ispnrm  21877  cmpfi  21946  txval  22102  xkoval  22125  ptval2  22139  ptpjopn  22150  xkoccn  22157  xkoptsub  22192  xkopt  22193  fmval  22481  fmf  22483  txflf  22544  cnextf  22604  subgntr  22644  opnsubg  22645  clsnsg  22647  snclseqg  22653  tsmsval2  22667  tsmsxplem1  22690  ustuqtoplem  22777  utopsnneiplem  22785  utopsnneip  22786  fmucndlem  22829  ressprdsds  22910  mopnval  22977  metuval  23088  metdsval  23384  lebnumlem1  23494  lebnumlem3  23496  pi1xfrcnvlem  23589  pi1xfrcnv  23590  minveclem3b  23960  elovolmr  24006  ovolctb  24020  ovoliunlem3  24034  ovolshftlem1  24039  voliunlem3  24082  voliun  24084  volsup  24086  uniioombllem2  24113  uniioombllem3  24115  mbflimsup  24196  itg1climres  24244  itg2monolem1  24280  itg2i1fseq  24285  itg2cnlem1  24291  ellimc2  24404  dvivth  24536  dvne0  24537  lhop2  24541  lhop  24542  mdegfval  24585  dchrptlem2  25769  dchrpt  25771  tglnunirn  26262  tgisline  26341  perpln1  26424  perpln2  26425  isperp  26426  ishpg  26473  lmif  26499  islmib  26501  edgval  26762  edgopval  26764  edgstruct  26766  uhgr2edg  26918  usgr1e  26955  cplgrop  27147  cusgrexi  27153  structtocusgr  27156  1loopgredg  27211  1egrvtxdg0  27221  umgr2v2eedg  27234  ex-ima  28149  bafval  28309  pj3i  29913  elimampt  30312  ofrn2  30316  ffsrn  30392  pfxrn2  30544  pfxrn3  30545  swrdrn2  30556  swrdrn3  30557  gsumzresunsn  30619  tocycfv  30679  tocycf  30687  trsp2cyc  30693  cycpmco2f1  30694  cycpmco2rn  30695  cycpmconjvlem  30711  cycpmconjslem2  30725  smatrcl  30961  ordtprsval  31061  ordtprsuni  31062  ordtcnvNEW  31063  ordtrestNEW  31064  ordtrest2NEW  31066  qqhval  31115  qqhval2  31123  prodindf  31182  esumval  31205  esumsnf  31223  esumrnmpt2  31227  esumfsupre  31230  esumsup  31248  sxval  31349  omsval  31451  omsfval  31452  carsggect  31476  sibf0  31492  sitgfval  31499  cvmlift3lem6  32469  satfrnmapom  32515  mvtval  32645  mvrsval  32650  mrsubvrs  32667  elmsubrn  32673  msubrn  32674  mstaval  32689  msubvrs  32705  mclsval  32708  trpredeq1  32957  trpredeq2  32958  trpredeq3  32959  filnetlem4  33627  mptsnunlem  34502  dissneqlem  34504  exrecfnlem  34543  ctbssinf  34570  poimirlem3  34777  poimirlem9  34783  poimirlem16  34790  poimirlem17  34791  poimirlem19  34793  poimirlem20  34794  poimirlem24  34798  poimirlem30  34804  poimirlem32  34806  mblfinlem2  34812  ovoliunnfl  34816  voliunnfl  34818  isrngo  35058  drngoi  35112  rngohomval  35125  rngoisoval  35138  idlval  35174  pridlval  35194  maxidlval  35200  igenval  35222  symrelim  35677  unidmqs  35770  lsatset  36008  docaffvalN  38139  docafvalN  38140  qsalrel  39005  mzpmfp  39224  eldiophb  39234  diophrw  39236  conrel1d  39888  iunrelexp0  39927  rntrclfv  39957  clsneibex  40332  neicvgbex  40342  rnsnf  41324  fsneqrn  41354  mptima2  41397  limsupval3  41853  limsupresre  41857  limsupresico  41861  limsuppnfdlem  41862  limsupvaluz  41869  limsupvaluzmpt  41878  limsupvaluz2  41899  supcnvlimsup  41901  supcnvlimsupmpt  41902  liminfval  41920  liminfval5  41926  limsupresxr  41927  liminfresxr  41928  liminfresico  41932  liminfvalxr  41944  fourierdlem60  42332  fourierdlem61  42333  sge0val  42529  sge0z  42538  sge0revalmpt  42541  sge0tsms  42543  sge0sup  42554  sge0split  42572  sge0fodjrnlem  42579  sge0seq  42609  meadjiunlem  42628  meaiuninclem  42643  omeiunle  42680  ovolval2lem  42806  ovolval4lem2  42813  ovolval5lem2  42816  ovolval5lem3  42817  ovolval5  42818  ovnovollem2  42820  smfsuplem2  42967  smfsup  42969  smfsupmpt  42970  smfinf  42973  smfinfmpt  42974  smflimsuplem1  42975  smflimsuplem2  42976  smflimsuplem4  42978  smflimsuplem5  42979  smflimsuplem7  42981  smflimsup  42983  fnrnafv  43242  afv2eq12d  43295
  Copyright terms: Public domain W3C validator