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

Theorem rneqd 5064
Description: Equality deduction for range. (Contributed by NM, 4-Mar-2004.)
Hypothesis
Ref Expression
rneqd.1  |-  ( ph  ->  A  =  B )
Assertion
Ref Expression
rneqd  |-  ( ph  ->  ran  A  =  ran  B )

Proof of Theorem rneqd
StepHypRef Expression
1 rneqd.1 . 2  |-  ( ph  ->  A  =  B )
2 rneq 5062 . 2  |-  ( A  =  B  ->  ran  A  =  ran  B )
31, 2syl 16 1  |-  ( ph  ->  ran  A  =  ran  B )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1649   ran crn 4846
This theorem is referenced by:  resima2  5146  imaeq1  5165  imaeq2  5166  csbima12gALT  5181  resiima  5187  rnxpid  5269  xpima  5280  elxp4  5324  elxp5  5325  funimacnv  5492  fnima  5530  2ndval  6319  fo2nd  6334  f2ndres  6336  curry1  6405  curry2  6408  oarec  6772  en1  7141  xpassen  7169  xpdom2  7170  sbthlem4  7187  fodomr  7225  dffi3  7402  marypha2lem4  7409  ordtypelem9  7459  dfac12lem1  7987  dfac12r  7990  fin23lem32  8188  fin23lem34  8190  fin23lem35  8191  fin23lem36  8192  fin23lem38  8193  fin23lem39  8194  fin23lem41  8196  itunitc  8265  ttukeylem3  8355  fpwwe2lem6  8474  fpwwe2lem9  8477  wunex2  8577  wuncval2  8586  gruima  8641  rpnnen1  10569  hashf1lem1  11667  limsupval  12231  xpnnenOLD  12772  vdwapfval  13302  vdwapval  13304  vdwmc  13309  vdwpc  13311  vdwlem6  13317  vdwlem8  13319  restval  13617  restid2  13621  prdsval  13641  prdsdsval  13663  prdsdsval2  13669  prdsdsval3  13670  imasval  13700  imasdsval  13704  isfull  14070  arwval  14161  gsumvalx  14737  conjsubg  15000  sylow1lem2  15196  sylow1lem4  15198  sylow1  15200  sylow2blem1  15217  sylow2b  15220  sylow3lem1  15224  sylow3lem2  15225  sylow3lem3  15226  sylow3lem5  15228  sylow3lem6  15229  sylow3  15230  lsmfval  15235  lsmvalx  15236  oppglsm  15239  subglsm  15268  lsmpropd  15272  efgval2  15319  efgi2  15320  efgtlen  15321  efgsdm  15325  efgsdmi  15327  efgsrel  15329  efgs1b  15331  efgsp1  15332  efgsres  15333  efgsfo  15334  efgrelexlemb  15345  frgpnabllem1  15447  iscyg  15452  iscyggen  15453  gsumxp  15513  dprdval  15524  ablfac2  15610  zncyg  16792  cygznlem2a  16811  tgrest  17185  ordtval  17215  ordtbas2  17217  ordtcnv  17227  ordtrest  17228  ordtrest2  17230  ispnrm  17365  cmpfi  17433  txval  17557  xkoval  17580  ptval2  17594  ptpjopn  17605  xkoccn  17612  xkoptsub  17647  xkopt  17648  fmval  17936  fmf  17938  txflf  17999  cnextf  18058  subgntr  18097  opnsubg  18098  clsnsg  18100  snclseqg  18106  tsmsval2  18120  tsmsxplem1  18143  ustuqtoplem  18230  utopsnneiplem  18238  utopsnneip  18239  fmucndlem  18282  ressprdsds  18362  mopnval  18429  metuvalOLD  18540  metuval  18541  metdsval  18838  lebnumlem1  18947  lebnumlem3  18949  pi1xfrcnvlem  19042  pi1xfrcnv  19043  minveclem3b  19290  elovolmr  19333  ovolctb  19347  ovoliunlem3  19361  ovolshftlem1  19366  voliunlem3  19407  voliun  19409  volsup  19411  uniioombllem2  19436  uniioombllem3  19438  mbflimsup  19519  itg1climres  19567  itg2monolem1  19603  itg2i1fseq  19608  itg2cnlem1  19614  ellimc2  19725  dvivth  19855  dvne0  19856  lhop2  19860  lhop  19861  evlseu  19898  mdegfval  19946  dchrptlem2  21010  dchrpt  21012  nbgraop  21397  ex-ima  21711  subgornss  21855  efghgrp  21922  isrngo  21927  drngoi  21956  vcoprne  22019  bafval  22044  pj3i  23672  ofrn2  24014  qqhval  24319  qqhval2  24327  esumval  24402  esumsn  24417  esumfsupre  24422  sxval  24505  sibf0  24610  sitgfval  24616  cvmlift3lem6  24972  relexprn  25097  trpredeq1  25445  trpredeq2  25446  trpredeq3  25447  mblfinlem  26151  ovoliunnfl  26155  voliunnfl  26157  filnetlem4  26308  rngohomval  26478  rngoisoval  26491  idlval  26521  pridlval  26541  maxidlval  26547  igenval  26569  mzpmfp  26702  eldiophb  26713  diophrw  26715  frlmsplit2  27119  pmtrfrn  27276  psgnfval  27299  fnrnafv  27901  lsatset  29485  docaffvalN  31616  docafvalN  31617
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2393
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2399  df-cleq 2405  df-clel 2408  df-nfc 2537  df-rab 2683  df-v 2926  df-dif 3291  df-un 3293  df-in 3295  df-ss 3302  df-nul 3597  df-if 3708  df-sn 3788  df-pr 3789  df-op 3791  df-br 4181  df-opab 4235  df-cnv 4853  df-dm 4855  df-rn 4856
  Copyright terms: Public domain W3C validator