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

Theorem rexbidva 2573
Description: Formula-building rule for restricted existential quantifier (deduction rule). (Contributed by NM, 9-Mar-1997.)
Hypothesis
Ref Expression
ralbidva.1  |-  ( (
ph  /\  x  e.  A )  ->  ( ps 
<->  ch ) )
Assertion
Ref Expression
rexbidva  |-  ( ph  ->  ( E. x  e.  A  ps  <->  E. x  e.  A  ch )
)
Distinct variable group:    ph, x
Allowed substitution hints:    ps( x)    ch( x)    A( x)

Proof of Theorem rexbidva
StepHypRef Expression
1 nfv 1609 . 2  |-  F/ x ph
2 ralbidva.1 . 2  |-  ( (
ph  /\  x  e.  A )  ->  ( ps 
<->  ch ) )
31, 2rexbida 2571 1  |-  ( ph  ->  ( E. x  e.  A  ps  <->  E. x  e.  A  ch )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    /\ wa 358    e. wcel 1696   E.wrex 2557
This theorem is referenced by:  2rexbiia  2590  2rexbidva  2597  rexeqbidva  2764  onfr  4447  frinxp  4771  dfimafn  5587  funimass4  5589  fconstfv  5750  fliftel  5824  fliftf  5830  isomin  5850  f1oiso  5864  releldm2  6186  oaass  6575  qsinxp  6751  qliftel  6757  fimaxg  7120  ordunifi  7123  supisolem  7237  wemapwe  7416  cflim2  7905  cfsmolem  7912  alephsing  7918  brdom7disj  8172  brdom6disj  8173  alephreg  8220  nqereu  8569  1idpr  8669  map2psrpr  8748  axsup  8914  rereccl  9494  sup3  9727  infm3  9729  creur  9756  creui  9757  nndiv  9802  nnrecl  9979  rpnnen1lem1  10358  rpnnen1lem2  10359  rpnnen1lem3  10360  rpnnen1lem5  10362  supxrbnd1  10656  supxrbnd2  10657  supxrbnd  10663  expnlbnd  11247  limsuplt  11969  clim2  11994  clim2c  11995  clim0c  11997  ello12  12006  elo12  12017  rlimresb  12055  climabs0  12075  sumeq2ii  12182  mertens  12358  alzdvds  12594  oddm1even  12604  divalglem4  12611  divalgb  12619  vdwlem6  13049  vdwlem11  13054  vdw  13057  ramval  13071  imasleval  13459  isipodrs  14280  ipodrsfi  14282  mndpropd  14414  grppropd  14516  conjnmzb  14733  sylow1lem2  14926  sylow3lem1  14954  sylow3lem3  14956  lsmelvalm  14978  lsmass  14995  iscyg3  15189  ghmcyg  15198  cycsubgcyg  15203  pgpfac1lem2  15326  pgpfac1lem4  15329  ablfac2  15340  dvdsr02  15454  crngunit  15460  dvdsrpropd  15494  lpigen  16024  znunit  16533  isclo  16840  iscnp3  16990  lmbrf  17006  cncnp  17025  lmss  17042  isnrm2  17102  cmpfi  17151  1stcfb  17187  1stccnp  17204  ptrescn  17349  txkgen  17362  xkoinjcn  17397  trfil3  17599  fmid  17671  lmflf  17716  txflf  17717  ptcmplem3  17764  tsmsf1o  17843  metrest  18086  metcnp  18103  metcnp2  18104  txmetcnp  18109  evth2  18474  lmmbrf  18704  iscfil2  18708  fmcfil  18714  iscau2  18719  iscau4  18721  iscauf  18722  caucfil  18725  iscmet3lem3  18732  cfilresi  18737  causs  18740  lmclim  18744  ivth2  18831  ovolfioo  18843  ovolficc  18844  ovolshftlem1  18884  ovolscalem1  18888  volsup2  18976  ismbf3d  19025  mbfaddlem  19031  mbfsup  19035  mbfinf  19036  itg2seq  19113  itg2gt0  19131  ellimc2  19243  ellimc3  19245  rolle  19353  cmvth  19354  mvth  19355  dvlip  19356  dvivth  19373  lhop1lem  19376  deg1ldg  19494  ulm2  19780  ulmdvlem3  19795  dcubic  20158  mcubic  20159  cubic2  20160  rlimcnp  20276  ftalem3  20328  isppw2  20369  lgsquadlem2  20610  dchrmusumlema  20658  dchrisum0lema  20679  nmobndi  21369  nmounbi  21370  nmoo0  21385  h2hcau  21575  h2hlm  21576  shsel3  21910  pjhtheu2  22011  chscllem2  22233  adjbdln  22679  branmfn  22701  pjimai  22772  chrelati  22960  cdj3lem3  23034  cdj3lem3b  23036  dfimafnf  23057  ballotlemodife  23072  lmdvg  23391  gsumpropd2lem  23394  erdszelem10  23746  iscvm  23805  cprodeq2ii  24135  zprod  24160  elfuns  24525  axsegcon  24627  axpasch  24641  axcontlem7  24670  seglelin  24811  outsideofeu  24826  supadd  24996  prl2  25272  prjmapcp2  25273  iscst4  25280  nZdef  25283  prodeq3ii  25411  osneisi  25634  bwt2  25695  lvsovso2  25730  supnuf  25732  supexr  25734  cnegvex2  25763  rnegvex2  25764  fnckle  26148  bhp2a  26279  opnrebl  26338  opnrebl2  26339  filnetlem4  26433  lmclim2  26577  caures  26579  isbnd3b  26612  heiborlem7  26644  heiborlem10  26647  rrncmslem  26659  isdrngo2  26692  prter3  26853  elrfirn  26873  elrfirn2  26874  mrefg3  26886  diophin  26955  diophun  26956  diophren  26999  rmxycomplete  27105  wepwsolem  27241  fnwe2lem2  27251  islssfg  27271  elfilspd  27358  dfaimafn  28133  islshpsm  29792  lsatfixedN  29821  lrelat  29826  eqlkr2  29912  lshpkrlem1  29922  lfl1dim  29933  eqlkr4  29977  ishlat3N  30166  hlsupr2  30198  hlrelat5N  30212  hlrelat  30213  cvrval5  30226  cvrat42  30255  athgt  30267  3dim0  30268  islln3  30321  llnexatN  30332  islpln3  30344  islvol3  30387  islvol5  30390  isline4N  30588  polval2N  30717  4atex3  30892  cdleme0ex2N  31035  cdlemefrs29cpre1  31209  cdlemb3  31417  cdlemg33c  31519  cdlemg33e  31521  dia1dim2  31874  cdlemm10N  31930  dib1dim2  31980  diclspsn  32006  dih1dimatlem  32141  dihatexv2  32151  djhcvat42  32227  dihjat1lem  32240  dvh4dimat  32250  dvh2dimatN  32252  lcfrlem9  32362  mapdval4N  32444  mapdcv  32472
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-11 1727
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1532  df-nf 1535  df-rex 2562
  Copyright terms: Public domain W3C validator