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

Theorem rexbidva 2560
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 1605 . 2  |-  F/ x ph
2 ralbidva.1 . 2  |-  ( (
ph  /\  x  e.  A )  ->  ( ps 
<->  ch ) )
31, 2rexbida 2558 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 1684   E.wrex 2544
This theorem is referenced by:  2rexbiia  2577  2rexbidva  2584  rexeqbidva  2751  onfr  4431  frinxp  4755  dfimafn  5571  funimass4  5573  fconstfv  5734  fliftel  5808  fliftf  5814  isomin  5834  f1oiso  5848  releldm2  6170  oaass  6559  qsinxp  6735  qliftel  6741  fimaxg  7104  ordunifi  7107  supisolem  7221  wemapwe  7400  cflim2  7889  cfsmolem  7896  alephsing  7902  brdom7disj  8156  brdom6disj  8157  alephreg  8204  nqereu  8553  1idpr  8653  map2psrpr  8732  axsup  8898  rereccl  9478  sup3  9711  infm3  9713  creur  9740  creui  9741  nndiv  9786  nnrecl  9963  rpnnen1lem1  10342  rpnnen1lem2  10343  rpnnen1lem3  10344  rpnnen1lem5  10346  supxrbnd1  10640  supxrbnd2  10641  supxrbnd  10647  expnlbnd  11231  limsuplt  11953  clim2  11978  clim2c  11979  clim0c  11981  ello12  11990  elo12  12001  rlimresb  12039  climabs0  12059  sumeq2ii  12166  mertens  12342  alzdvds  12578  oddm1even  12588  divalglem4  12595  divalgb  12603  vdwlem6  13033  vdwlem11  13038  vdw  13041  ramval  13055  imasleval  13443  isipodrs  14264  ipodrsfi  14266  mndpropd  14398  grppropd  14500  conjnmzb  14717  sylow1lem2  14910  sylow3lem1  14938  sylow3lem3  14940  lsmelvalm  14962  lsmass  14979  iscyg3  15173  ghmcyg  15182  cycsubgcyg  15187  pgpfac1lem2  15310  pgpfac1lem4  15313  ablfac2  15324  dvdsr02  15438  crngunit  15444  dvdsrpropd  15478  lpigen  16008  znunit  16517  isclo  16824  iscnp3  16974  lmbrf  16990  cncnp  17009  lmss  17026  isnrm2  17086  cmpfi  17135  1stcfb  17171  1stccnp  17188  ptrescn  17333  txkgen  17346  xkoinjcn  17381  trfil3  17583  fmid  17655  lmflf  17700  txflf  17701  ptcmplem3  17748  tsmsf1o  17827  metrest  18070  metcnp  18087  metcnp2  18088  txmetcnp  18093  evth2  18458  lmmbrf  18688  iscfil2  18692  fmcfil  18698  iscau2  18703  iscau4  18705  iscauf  18706  caucfil  18709  iscmet3lem3  18716  cfilresi  18721  causs  18724  lmclim  18728  ivth2  18815  ovolfioo  18827  ovolficc  18828  ovolshftlem1  18868  ovolscalem1  18872  volsup2  18960  ismbf3d  19009  mbfaddlem  19015  mbfsup  19019  mbfinf  19020  itg2seq  19097  itg2gt0  19115  ellimc2  19227  ellimc3  19229  rolle  19337  cmvth  19338  mvth  19339  dvlip  19340  dvivth  19357  lhop1lem  19360  deg1ldg  19478  ulm2  19764  ulmdvlem3  19779  dcubic  20142  mcubic  20143  cubic2  20144  rlimcnp  20260  ftalem3  20312  isppw2  20353  lgsquadlem2  20594  dchrmusumlema  20642  dchrisum0lema  20663  nmobndi  21353  nmounbi  21354  nmoo0  21369  h2hcau  21559  h2hlm  21560  shsel3  21894  pjhtheu2  21995  chscllem2  22217  adjbdln  22663  branmfn  22685  pjimai  22756  chrelati  22944  cdj3lem3  23018  cdj3lem3b  23020  dfimafnf  23041  ballotlemodife  23056  lmdvg  23376  gsumpropd2lem  23379  erdszelem10  23731  iscvm  23790  elfuns  24454  axsegcon  24555  axpasch  24569  axcontlem7  24598  seglelin  24739  outsideofeu  24754  prl2  25169  prjmapcp2  25170  iscst4  25177  nZdef  25180  prodeq3ii  25308  osneisi  25531  bwt2  25592  lvsovso2  25627  supnuf  25629  supexr  25631  cnegvex2  25660  rnegvex2  25661  fnckle  26045  bhp2a  26176  opnrebl  26235  opnrebl2  26236  filnetlem4  26330  lmclim2  26474  caures  26476  isbnd3b  26509  heiborlem7  26541  heiborlem10  26544  rrncmslem  26556  isdrngo2  26589  prter3  26750  elrfirn  26770  elrfirn2  26771  mrefg3  26783  diophin  26852  diophun  26853  diophren  26896  rmxycomplete  27002  wepwsolem  27138  fnwe2lem2  27148  islssfg  27168  elfilspd  27255  dfaimafn  28027  islshpsm  29170  lsatfixedN  29199  lrelat  29204  eqlkr2  29290  lshpkrlem1  29300  lfl1dim  29311  eqlkr4  29355  ishlat3N  29544  hlsupr2  29576  hlrelat5N  29590  hlrelat  29591  cvrval5  29604  cvrat42  29633  athgt  29645  3dim0  29646  islln3  29699  llnexatN  29710  islpln3  29722  islvol3  29765  islvol5  29768  isline4N  29966  polval2N  30095  4atex3  30270  cdleme0ex2N  30413  cdlemefrs29cpre1  30587  cdlemb3  30795  cdlemg33c  30897  cdlemg33e  30899  dia1dim2  31252  cdlemm10N  31308  dib1dim2  31358  diclspsn  31384  dih1dimatlem  31519  dihatexv2  31529  djhcvat42  31605  dihjat1lem  31618  dvh4dimat  31628  dvh2dimatN  31630  lcfrlem9  31740  mapdval4N  31822  mapdcv  31850
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-11 1715
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1529  df-nf 1532  df-rex 2549
  Copyright terms: Public domain W3C validator