Theorem rexbidva 2683

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 1626	. 2 |- F/ x ph
2		ralbidva.1	. 2 |- ( ( ph /\ x e. A ) -> ( ps <-> ch ) )
3	1, 2	rexbida 2681	1 |- ( ph -> ( E. x e. A ps <-> E. x e. A ch ) )

Syntax hints:   -> wi 4   <-> wb 177   /\ wa 359   e. wcel 1721   E.wrex 2667

This theorem is referenced by:  2rexbiia  2700  2rexbidva  2707  rexeqbidva  2879  onfr  4580  frinxp  4902  dfimafn  5734  funimass4  5736  fconstfv  5913  fliftel  5990  fliftf  5996  isomin  6016  f1oiso  6030  releldm2  6356  oaass  6763  qsinxp  6939  qliftel  6946  fimaxg  7313  ordunifi  7316  supisolem  7431  wemapwe  7610  cflim2  8099  cfsmolem  8106  alephsing  8112  brdom7disj  8365  brdom6disj  8366  alephreg  8413  nqereu  8762  1idpr  8862  map2psrpr  8941  axsup  9107  rereccl  9688  sup3  9921  infm3  9923  creur  9950  creui  9951  nndiv  9996  nnrecl  10175  rpnnen1lem1  10556  rpnnen1lem2  10557  rpnnen1lem3  10558  rpnnen1lem5  10560  supxrbnd1  10856  supxrbnd2  10857  supxrbnd  10863  expnlbnd  11464  limsuplt  12228  clim2  12253  clim2c  12254  clim0c  12256  ello12  12265  elo12  12276  rlimresb  12314  climabs0  12334  sumeq2ii  12442  mertens  12618  alzdvds  12854  oddm1even  12864  divalglem4  12871  divalgb  12879  vdwlem6  13309  vdwlem11  13314  vdw  13317  ramval  13331  imasleval  13721  isipodrs  14542  ipodrsfi  14544  mndpropd  14676  grppropd  14778  conjnmzb  14995  sylow1lem2  15188  sylow3lem1  15216  sylow3lem3  15218  lsmelvalm  15240  lsmass  15257  iscyg3  15451  ghmcyg  15460  cycsubgcyg  15465  pgpfac1lem2  15588  pgpfac1lem4  15591  ablfac2  15602  dvdsr02  15716  crngunit  15722  dvdsrpropd  15756  lpigen  16282  znunit  16799  isclo  17106  iscnp3  17262  lmbrf  17278  cncnp  17298  lmss  17316  isnrm2  17376  cmpfi  17425  1stcfb  17461  1stccnp  17478  ptrescn  17624  txkgen  17637  xkoinjcn  17672  trfil3  17873  fmid  17945  lmflf  17990  txflf  17991  ptcmplem3  18038  tsmsf1o  18127  ucnprima  18265  metrest  18507  metcnp  18524  metcnp2  18525  txmetcnp  18530  metuel2  18562  metustblOLD  18563  metustbl  18564  metutopOLD  18565  psmetutop  18566  metucnOLD  18571  metucn  18572  evth2  18938  lmmbrf  19168  iscfil2  19172  fmcfil  19178  iscau2  19183  iscau4  19185  iscauf  19186  caucfil  19189  iscmet3lem3  19196  cfilresi  19201  causs  19204  lmclim  19208  ivth2  19305  ovolfioo  19317  ovolficc  19318  ovolshftlem1  19358  ovolscalem1  19362  volsup2  19450  ismbf3d  19499  mbfaddlem  19505  mbfsup  19509  mbfinf  19510  itg2seq  19587  itg2gt0  19605  ellimc2  19717  ellimc3  19719  rolle  19827  cmvth  19828  mvth  19829  dvlip  19830  dvivth  19847  lhop1lem  19850  deg1ldg  19968  ulm2  20254  ulmdvlem3  20271  dcubic  20639  mcubic  20640  cubic2  20641  rlimcnp  20757  ftalem3  20810  isppw2  20851  lgsquadlem2  21092  dchrmusumlema  21140  dchrisum0lema  21161  nmobndi  22229  nmounbi  22230  nmoo0  22245  h2hcau  22435  h2hlm  22436  shsel3  22770  pjhtheu2  22871  chscllem2  23093  adjbdln  23539  branmfn  23561  pjimai  23632  chrelati  23820  cdj3lem3  23894  cdj3lem3b  23896  dfimafnf  23996  ofpreima  24034  gsumpropd2lem  24173  isarchi2  24208  lmdvg  24291  esumfsup  24413  dya2icoseg2  24581  ballotlemodife  24708  ballotlemsima  24726  erdszelem10  24839  iscvm  24899  prodeq2ii  25192  zprod  25216  elfuns  25668  axsegcon  25770  axpasch  25784  axcontlem7  25813  seglelin  25954  outsideofeu  25969  supadd  26138  mblfinlem  26143  opnrebl  26213  opnrebl2  26214  filnetlem4  26300  lmclim2  26354  caures  26356  isbnd3b  26384  heiborlem7  26416  heiborlem10  26419  rrncmslem  26431  isdrngo2  26464  prter3  26621  elrfirn  26639  elrfirn2  26640  mrefg3  26652  diophin  26721  diophun  26722  diophren  26764  rmxycomplete  26870  wepwsolem  27006  fnwe2lem2  27016  islssfg  27036  elfilspd  27123  dfaimafn  27896  usgra2pth0  28042  el2spthonot0  28068  usg2spthonot1  28087  usgreg2spot  28170  islshpsm  29463  lsatfixedN  29492  lrelat  29497  eqlkr2  29583  lshpkrlem1  29593  lfl1dim  29604  eqlkr4  29648  ishlat3N  29837  hlsupr2  29869  hlrelat5N  29883  hlrelat  29884  cvrval5  29897  cvrat42  29926  athgt  29938  3dim0  29939  islln3  29992  llnexatN  30003  islpln3  30015  islvol3  30058  islvol5  30061  isline4N  30259  polval2N  30388  4atex3  30563  cdleme0ex2N  30706  cdlemefrs29cpre1  30880  cdlemb3  31088  cdlemg33c  31190  cdlemg33e  31192  dia1dim2  31545  cdlemm10N  31601  dib1dim2  31651  diclspsn  31677  dih1dimatlem  31812  dihatexv2  31822  djhcvat42  31898  dihjat1lem  31911  dvh4dimat  31921  dvh2dimatN  31923  lcfrlem9  32033  mapdval4N  32115  mapdcv  32143

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-11 1757

This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1548  df-nf 1551  df-rex 2672