Theorem rexbidva 2727

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

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-12 1792

This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1587  df-nf 1590  df-rex 2716

This theorem is referenced by:  2rexbiia  2744  2rexbidva  2751  rexeqbidva  2929  onfr  4753  frinxp  4899  dfimafn  5735  funimass4  5737  fconstfv  5935  fliftel  5997  fliftf  6003  isomin  6023  f1oiso  6037  releldm2  6619  oaass  6992  qsinxp  7168  qliftel  7175  fimaxg  7551  ordunifi  7554  supisolem  7712  wemapwe  7920  wemapweOLD  7921  cflim2  8424  cfsmolem  8431  alephsing  8437  brdom7disj  8690  brdom6disj  8691  alephreg  8738  nqereu  9090  1idpr  9190  map2psrpr  9269  axsup  9442  rereccl  10041  sup3  10279  infm3  10281  creur  10308  creui  10309  nndiv  10354  nnrecl  10569  rpnnen1lem1  10971  rpnnen1lem2  10972  rpnnen1lem3  10973  rpnnen1lem5  10975  supxrbnd1  11276  supxrbnd2  11277  supxrbnd  11283  expnlbnd  11986  limsuplt  12949  clim2  12974  clim2c  12975  clim0c  12977  ello12  12986  elo12  12997  rlimresb  13035  climabs0  13055  sumeq2ii  13162  mertens  13338  alzdvds  13575  oddm1even  13585  divalglem4  13592  divalgb  13600  modprmn0modprm0  13867  vdwlem6  14039  vdwlem11  14044  vdw  14047  ramval  14061  imasleval  14471  isipodrs  15323  ipodrsfi  15325  mndpropd  15438  gsumpropd2lem  15496  grppropd  15547  conjnmzb  15772  symgextfo  15918  symgfixfo  15936  sylow1lem2  16089  sylow3lem1  16117  sylow3lem3  16119  lsmelvalm  16141  lsmass  16158  iscyg3  16354  ghmcyg  16363  cycsubgcyg  16368  pgpfac1lem2  16566  pgpfac1lem4  16569  ablfac2  16580  dvdsr02  16738  crngunit  16744  dvdsrpropd  16778  lpigen  17318  znunit  17976  elfilspd  18212  symgmatr01  18440  isclo  18671  iscnp3  18828  lmbrf  18844  cncnp  18864  lmss  18882  isnrm2  18942  cmpfi  18991  bwthOLD  18994  1stcfb  19029  1stccnp  19046  ptrescn  19192  txkgen  19205  xkoinjcn  19240  trfil3  19441  fmid  19513  lmflf  19558  txflf  19559  ptcmplem3  19606  tsmsf1o  19699  ucnprima  19837  metrest  20079  metcnp  20096  metcnp2  20097  txmetcnp  20102  metuel2  20134  metustblOLD  20135  metustbl  20136  metutopOLD  20137  psmetutop  20138  metucnOLD  20143  metucn  20144  evth2  20512  lmmbrf  20753  iscfil2  20757  fmcfil  20763  iscau2  20768  iscau4  20770  iscauf  20771  caucfil  20774  iscmet3lem3  20781  cfilresi  20786  causs  20789  lmclim  20793  ivth2  20919  ovolfioo  20931  ovolficc  20932  ovolshftlem1  20972  ovolscalem1  20976  volsup2  21065  ismbf3d  21112  mbfaddlem  21118  mbfsup  21122  mbfinf  21123  itg2seq  21200  itg2gt0  21218  ellimc2  21332  ellimc3  21334  rolle  21442  cmvth  21443  mvth  21444  dvlip  21445  dvivth  21462  lhop1lem  21465  deg1ldg  21543  ulm2  21830  ulmdvlem3  21847  dcubic  22221  mcubic  22222  cubic2  22223  rlimcnp  22339  ftalem3  22392  isppw2  22433  lgsquadlem2  22674  dchrmusumlema  22722  dchrisum0lema  22743  tglowdim2l  23033  mirreu3  23038  axsegcon  23141  axpasch  23155  axcontlem7  23184  nmobndi  24143  nmounbi  24144  nmoo0  24159  h2hcau  24349  h2hlm  24350  shsel3  24686  pjhtheu2  24787  chscllem2  25009  adjbdln  25455  branmfn  25477  pjimai  25548  chrelati  25736  cdj3lem3  25810  cdj3lem3b  25812  dfimafnf  25918  ofpreima  25952  isarchi2  26170  submarchi  26171  archirng  26173  archiabl  26183  isarchiofld  26253  lmdvg  26352  esumfsup  26488  dya2icoseg2  26662  eulerpartlemgh  26730  ballotlemodife  26849  ballotlemsima  26867  erdszelem10  27057  iscvm  27117  prodeq2ii  27395  zprod  27419  wsuclem  27731  seglelin  28116  outsideofeu  28131  supadd  28389  ptrest  28396  mblfinlem1  28399  opnrebl  28486  opnrebl2  28487  filnetlem4  28573  lmclim2  28625  caures  28627  isbnd3b  28655  heiborlem7  28687  heiborlem10  28690  rrncmslem  28702  isdrngo2  28735  prter3  28998  elrfirn  29002  elrfirn2  29003  mrefg3  29015  diophin  29082  diophun  29083  diophren  29123  rmxycomplete  29229  wepwsolem  29365  fnwe2lem2  29375  islssfg  29394  dfaimafn  30042  usgra2pth0  30273  el2spthonot0  30361  usg2spthonot1  30380  clwwlkfo  30430  eclclwwlkn1  30477  rusgranumwlks  30545  usgreg2spot  30631  rabssnn0fi  30716  mptnn0fsupp  30771  bj-finsumval0  32479  islshpsm  32518  lsatfixedN  32547  lrelat  32552  eqlkr2  32638  lshpkrlem1  32648  lfl1dim  32659  eqlkr4  32703  ishlat3N  32892  hlsupr2  32924  hlrelat5N  32938  hlrelat  32939  cvrval5  32952  cvrat42  32981  athgt  32993  3dim0  32994  islln3  33047  llnexatN  33058  islpln3  33070  islvol3  33113  islvol5  33116  isline4N  33314  polval2N  33443  4atex3  33618  cdleme0ex2N  33761  cdlemefrs29cpre1  33935  cdlemb3  34143  cdlemg33c  34245  cdlemg33e  34247  dia1dim2  34600  cdlemm10N  34656  dib1dim2  34706  diclspsn  34732  dih1dimatlem  34867  dihatexv2  34877  djhcvat42  34953  dihjat1lem  34966  dvh4dimat  34976  dvh2dimatN  34978  lcfrlem9  35088  mapdval4N  35170  mapdcv  35198