Theorem rexbidva 2842

Description: Formula-building rule for restricted existential quantifier (deduction rule). (Contributed by NM, 9-Mar-1997.)

Hypothesis

Ref	Expression
rexbidva.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

Step	Hyp	Ref	Expression
1		nfv 1674	. 2 |- F/ x ph
2		rexbidva.1	. 2 |- ( ( ph /\ x e. A ) -> ( ps <-> ch ) )
3	1, 2	rexbida 2841	1 |- ( ph -> ( E. x e. A ps <-> E. x e. A ch ) )

Syntax hints:   -> wi 4   <-> wb 184   /\ wa 369   e. wcel 1758   E.wrex 2796

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-12 1794

This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1588  df-nf 1591  df-rex 2801

This theorem is referenced by:  2rexbiia  2853  2rexbidva  2860  rexeqbidva  3030  onfr  4856  frinxp  5002  dfimafn  5839  funimass4  5841  fconstfv  6039  fliftel  6101  fliftf  6107  isomin  6127  f1oiso  6141  releldm2  6724  oaass  7100  qsinxp  7276  qliftel  7283  fimaxg  7660  ordunifi  7663  supisolem  7821  wemapwe  8029  wemapweOLD  8030  cflim2  8533  cfsmolem  8540  alephsing  8546  brdom7disj  8799  brdom6disj  8800  alephreg  8847  nqereu  9199  1idpr  9299  map2psrpr  9378  axsup  9551  rereccl  10150  sup3  10388  infm3  10390  creur  10417  creui  10418  nndiv  10463  nnrecl  10678  rpnnen1lem1  11080  rpnnen1lem2  11081  rpnnen1lem3  11082  rpnnen1lem5  11084  supxrbnd1  11385  supxrbnd2  11386  supxrbnd  11392  expnlbnd  12095  limsuplt  13059  clim2  13084  clim2c  13085  clim0c  13087  ello12  13096  elo12  13107  rlimresb  13145  climabs0  13165  sumeq2ii  13272  mertens  13448  alzdvds  13685  oddm1even  13695  divalglem4  13702  divalgb  13710  modprmn0modprm0  13977  vdwlem6  14149  vdwlem11  14154  vdw  14157  ramval  14171  imasleval  14581  isipodrs  15433  ipodrsfi  15435  mndpropd  15548  gsumpropd2lem  15607  grppropd  15658  conjnmzb  15883  symgextfo  16029  symgfixfo  16047  sylow1lem2  16202  sylow3lem1  16230  sylow3lem3  16232  lsmelvalm  16254  lsmass  16271  iscyg3  16467  ghmcyg  16476  cycsubgcyg  16481  pgpfac1lem2  16681  pgpfac1lem4  16684  ablfac2  16695  dvdsr02  16854  crngunit  16860  dvdsrpropd  16894  lpigen  17444  znunit  18105  elfilspd  18341  symgmatr01  18576  isclo  18807  iscnp3  18964  lmbrf  18980  cncnp  19000  lmss  19018  isnrm2  19078  cmpfi  19127  bwthOLD  19130  1stcfb  19165  1stccnp  19182  ptrescn  19328  txkgen  19341  xkoinjcn  19376  trfil3  19577  fmid  19649  lmflf  19694  txflf  19695  ptcmplem3  19742  tsmsf1o  19835  ucnprima  19973  metrest  20215  metcnp  20232  metcnp2  20233  txmetcnp  20238  metuel2  20270  metustblOLD  20271  metustbl  20272  metutopOLD  20273  psmetutop  20274  metucnOLD  20279  metucn  20280  evth2  20648  lmmbrf  20889  iscfil2  20893  fmcfil  20899  iscau2  20904  iscau4  20906  iscauf  20907  caucfil  20910  iscmet3lem3  20917  cfilresi  20922  causs  20925  lmclim  20929  ivth2  21055  ovolfioo  21067  ovolficc  21068  ovolshftlem1  21108  ovolscalem1  21112  volsup2  21201  ismbf3d  21248  mbfaddlem  21254  mbfsup  21258  mbfinf  21259  itg2seq  21336  itg2gt0  21354  ellimc2  21468  ellimc3  21470  rolle  21578  cmvth  21579  mvth  21580  dvlip  21581  dvivth  21598  lhop1lem  21601  deg1ldg  21679  ulm2  21966  ulmdvlem3  21983  dcubic  22357  mcubic  22358  cubic2  22359  rlimcnp  22475  ftalem3  22528  isppw2  22569  lgsquadlem2  22810  dchrmusumlema  22858  dchrisum0lema  22879  tglowdim2l  23178  mirreu3  23184  axsegcon  23308  axpasch  23322  axcontlem7  23351  nmobndi  24310  nmounbi  24311  nmoo0  24326  h2hcau  24516  h2hlm  24517  shsel3  24853  pjhtheu2  24954  chscllem2  25176  adjbdln  25622  branmfn  25644  pjimai  25715  chrelati  25903  cdj3lem3  25977  cdj3lem3b  25979  dfimafnf  26084  ofpreima  26118  isarchi2  26336  submarchi  26337  archirng  26339  archiabl  26349  isarchiofld  26419  lmdvg  26517  esumfsup  26653  dya2icoseg2  26827  eulerpartlemgh  26895  ballotlemodife  27014  ballotlemsima  27032  erdszelem10  27222  iscvm  27282  prodeq2ii  27560  zprod  27584  wsuclem  27896  seglelin  28281  outsideofeu  28296  supadd  28556  ptrest  28563  mblfinlem1  28566  opnrebl  28653  opnrebl2  28654  filnetlem4  28740  lmclim2  28792  caures  28794  isbnd3b  28822  heiborlem7  28854  heiborlem10  28857  rrncmslem  28869  isdrngo2  28902  prter3  29165  elrfirn  29169  elrfirn2  29170  mrefg3  29182  diophin  29249  diophun  29250  diophren  29290  rmxycomplete  29396  wepwsolem  29532  fnwe2lem2  29542  islssfg  29561  dfaimafn  30209  usgra2pth0  30440  el2spthonot0  30528  usg2spthonot1  30547  clwwlkfo  30597  eclclwwlkn1  30644  rusgranumwlks  30712  usgreg2spot  30798  rabssnn0fi  30885  mptnn0fsupp  30940  pmatcollpwfsupp  31229  pmattomply1mhmlem0  31272  pmattomply1mhmlem1  31273  bj-finsumval0  32889  islshpsm  32931  lsatfixedN  32960  lrelat  32965  eqlkr2  33051  lshpkrlem1  33061  lfl1dim  33072  eqlkr4  33116  ishlat3N  33305  hlsupr2  33337  hlrelat5N  33351  hlrelat  33352  cvrval5  33365  cvrat42  33394  athgt  33406  3dim0  33407  islln3  33460  llnexatN  33471  islpln3  33483  islvol3  33526  islvol5  33529  isline4N  33727  polval2N  33856  4atex3  34031  cdleme0ex2N  34174  cdlemefrs29cpre1  34348  cdlemb3  34556  cdlemg33c  34658  cdlemg33e  34660  dia1dim2  35013  cdlemm10N  35069  dib1dim2  35119  diclspsn  35145  dih1dimatlem  35280  dihatexv2  35290  djhcvat42  35366  dihjat1lem  35379  dvh4dimat  35389  dvh2dimatN  35391  lcfrlem9  35501  mapdval4N  35583  mapdcv  35611