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

Theorem rneqd 5801
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 5799 . 2 (𝐴 = 𝐵 → ran 𝐴 = ran 𝐵)
31, 2syl 17 1 (𝜑 → ran 𝐴 = ran 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1528  ran crn 5549
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 2790
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 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-rab 3144  df-v 3494  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-nul 4289  df-if 4464  df-sn 4558  df-pr 4560  df-op 4564  df-br 5058  df-opab 5120  df-cnv 5556  df-dm 5558  df-rn 5559
This theorem is referenced by:  resima2  5881  imaeq1  5917  imaeq2  5918  resiima  5937  rnxpid  6023  xpima  6032  funimacnv  6428  fnima  6471  rnfvprc  6657  elxp4  7616  elxp5  7617  2ndval  7681  fo2nd  7699  f2ndres  7703  curry1  7788  curry2  7791  oarec  8177  en1  8564  xpassen  8599  xpdom2  8600  sbthlem4  8618  fodomr  8656  dffi3  8883  marypha2lem4  8890  ordtypelem9  8978  dfac12lem1  9557  dfac12r  9560  fin23lem32  9754  fin23lem34  9756  fin23lem35  9757  fin23lem36  9758  fin23lem38  9759  fin23lem39  9760  fin23lem41  9762  itunitc  9831  ttukeylem3  9921  fpwwe2lem6  10045  fpwwe2lem9  10048  wunex2  10148  wuncval2  10157  gruima  10212  rpnnen1lem6  12369  hashf1lem1  13801  s1rn  13941  relexprng  14393  relexpfld  14396  limsupval  14819  vdwapfval  16295  vdwapval  16297  vdwmc  16302  vdwpc  16304  vdwlem6  16310  vdwlem8  16312  restval  16688  restid2  16692  prdsval  16716  prdsdsval  16739  prdsdsval2  16745  prdsdsval3  16746  imasval  16772  imasdsval  16776  isfull  17168  arwval  17291  gsumvalx  17874  conjsubg  18328  psgnfval  18557  sylow1lem2  18653  sylow1lem4  18655  sylow1  18657  sylow2blem1  18674  sylow2b  18677  sylow3lem1  18681  sylow3lem2  18682  sylow3lem3  18683  sylow3lem5  18685  sylow3lem6  18686  sylow3  18687  lsmfval  18692  lsmvalx  18693  oppglsm  18696  subglsm  18728  lsmpropd  18732  efgval2  18779  efgi2  18780  efgtlen  18781  efgsdm  18785  efgsdmi  18787  efgsrel  18789  efgs1b  18791  efgsp1  18792  efgsres  18793  efgsfo  18794  efgrelexlemb  18805  frgpnabllem1  18922  iscyg  18927  iscyggen  18928  gsumxp  19025  dprdval  19054  ablfac2  19140  rnrhmsubrg  19496  evlseu  20224  zncyg  20623  cygznlem2a  20642  frlmsplit2  20845  tgrest  21695  ordtval  21725  ordtbas2  21727  ordtcnv  21737  ordtrest  21738  ordtrest2  21740  ispnrm  21875  cmpfi  21944  txval  22100  xkoval  22123  ptval2  22137  ptpjopn  22148  xkoccn  22155  xkoptsub  22190  xkopt  22191  fmval  22479  fmf  22481  txflf  22542  cnextf  22602  subgntr  22642  opnsubg  22643  clsnsg  22645  snclseqg  22651  tsmsval2  22665  tsmsxplem1  22688  ustuqtoplem  22775  utopsnneiplem  22783  utopsnneip  22784  fmucndlem  22827  ressprdsds  22908  mopnval  22975  metuval  23086  metdsval  23382  lebnumlem1  23492  lebnumlem3  23494  pi1xfrcnvlem  23587  pi1xfrcnv  23588  minveclem3b  23958  elovolmr  24004  ovolctb  24018  ovoliunlem3  24032  ovolshftlem1  24037  voliunlem3  24080  voliun  24082  volsup  24084  uniioombllem2  24111  uniioombllem3  24113  mbflimsup  24194  itg1climres  24242  itg2monolem1  24278  itg2i1fseq  24283  itg2cnlem1  24289  ellimc2  24402  dvivth  24534  dvne0  24535  lhop2  24539  lhop  24540  mdegfval  24583  dchrptlem2  25768  dchrpt  25770  tglnunirn  26261  tgisline  26340  perpln1  26423  perpln2  26424  isperp  26425  ishpg  26472  lmif  26498  islmib  26500  edgval  26761  edgopval  26763  edgstruct  26765  uhgr2edg  26917  usgr1e  26954  cplgrop  27146  cusgrexi  27152  structtocusgr  27155  1loopgredg  27210  1egrvtxdg0  27220  umgr2v2eedg  27233  ex-ima  28148  bafval  28308  pj3i  29912  elimampt  30311  ofrn2  30315  ffsrn  30391  pfxrn2  30543  pfxrn3  30544  swrdrn2  30555  swrdrn3  30556  gsumzresunsn  30618  tocycfv  30678  tocycf  30686  trsp2cyc  30692  cycpmco2f1  30693  cycpmco2rn  30694  cycpmconjvlem  30710  cycpmconjslem2  30724  smatrcl  30960  ordtprsval  31060  ordtprsuni  31061  ordtcnvNEW  31062  ordtrestNEW  31063  ordtrest2NEW  31065  qqhval  31114  qqhval2  31122  prodindf  31181  esumval  31204  esumsnf  31222  esumrnmpt2  31226  esumfsupre  31229  esumsup  31247  sxval  31348  omsval  31450  omsfval  31451  carsggect  31475  sibf0  31491  sitgfval  31498  cvmlift3lem6  32468  satfrnmapom  32514  mvtval  32644  mvrsval  32649  mrsubvrs  32666  elmsubrn  32672  msubrn  32673  mstaval  32688  msubvrs  32704  mclsval  32707  trpredeq1  32956  trpredeq2  32957  trpredeq3  32958  filnetlem4  33626  mptsnunlem  34501  dissneqlem  34503  exrecfnlem  34542  ctbssinf  34569  poimirlem3  34776  poimirlem9  34782  poimirlem16  34789  poimirlem17  34790  poimirlem19  34792  poimirlem20  34793  poimirlem24  34797  poimirlem30  34803  poimirlem32  34805  mblfinlem2  34811  ovoliunnfl  34815  voliunnfl  34817  isrngo  35056  drngoi  35110  rngohomval  35123  rngoisoval  35136  idlval  35172  pridlval  35192  maxidlval  35198  igenval  35220  symrelim  35675  unidmqs  35768  lsatset  36006  docaffvalN  38137  docafvalN  38138  qsalrel  39003  mzpmfp  39222  eldiophb  39232  diophrw  39234  conrel1d  39886  iunrelexp0  39925  rntrclfv  39955  clsneibex  40330  neicvgbex  40340  rnsnf  41320  fsneqrn  41350  mptima2  41393  limsupval3  41849  limsupresre  41853  limsupresico  41857  limsuppnfdlem  41858  limsupvaluz  41865  limsupvaluzmpt  41874  limsupvaluz2  41895  supcnvlimsup  41897  supcnvlimsupmpt  41898  liminfval  41916  liminfval5  41922  limsupresxr  41923  liminfresxr  41924  liminfresico  41928  liminfvalxr  41940  fourierdlem60  42328  fourierdlem61  42329  sge0val  42525  sge0z  42534  sge0revalmpt  42537  sge0tsms  42539  sge0sup  42550  sge0split  42568  sge0fodjrnlem  42575  sge0seq  42605  meadjiunlem  42624  meaiuninclem  42639  omeiunle  42676  ovolval2lem  42802  ovolval4lem2  42809  ovolval5lem2  42812  ovolval5lem3  42813  ovolval5  42814  ovnovollem2  42816  smfsuplem2  42963  smfsup  42965  smfsupmpt  42966  smfinf  42969  smfinfmpt  42970  smflimsuplem1  42971  smflimsuplem2  42972  smflimsuplem4  42974  smflimsuplem5  42975  smflimsuplem7  42977  smflimsup  42979  fnrnafv  43238  afv2eq12d  43291
  Copyright terms: Public domain W3C validator