Theorem rexbidva 2722

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-12 1791

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

This theorem is referenced by:  2rexbiia  2739  2rexbidva  2746  rexeqbidva  2924  onfr  4745  frinxp  4891  dfimafn  5728  funimass4  5730  fconstfv  5927  fliftel  5989  fliftf  5995  isomin  6015  f1oiso  6029  releldm2  6613  oaass  6988  qsinxp  7164  qliftel  7171  fimaxg  7547  ordunifi  7550  supisolem  7708  wemapwe  7916  wemapweOLD  7917  cflim2  8420  cfsmolem  8427  alephsing  8433  brdom7disj  8686  brdom6disj  8687  alephreg  8734  nqereu  9085  1idpr  9185  map2psrpr  9264  axsup  9437  rereccl  10036  sup3  10274  infm3  10276  creur  10303  creui  10304  nndiv  10349  nnrecl  10564  rpnnen1lem1  10966  rpnnen1lem2  10967  rpnnen1lem3  10968  rpnnen1lem5  10970  supxrbnd1  11271  supxrbnd2  11272  supxrbnd  11278  expnlbnd  11977  limsuplt  12940  clim2  12965  clim2c  12966  clim0c  12968  ello12  12977  elo12  12988  rlimresb  13026  climabs0  13046  sumeq2ii  13153  mertens  13328  alzdvds  13565  oddm1even  13575  divalglem4  13582  divalgb  13590  modprmn0modprm0  13857  vdwlem6  14029  vdwlem11  14034  vdw  14037  ramval  14051  imasleval  14461  isipodrs  15313  ipodrsfi  15315  mndpropd  15428  grppropd  15535  conjnmzb  15760  symgextfo  15906  symgfixfo  15924  sylow1lem2  16077  sylow3lem1  16105  sylow3lem3  16107  lsmelvalm  16129  lsmass  16146  iscyg3  16342  ghmcyg  16351  cycsubgcyg  16356  pgpfac1lem2  16549  pgpfac1lem4  16552  ablfac2  16563  dvdsr02  16681  crngunit  16687  dvdsrpropd  16721  lpigen  17259  znunit  17837  elfilspd  18073  symgmatr01  18301  isclo  18532  iscnp3  18689  lmbrf  18705  cncnp  18725  lmss  18743  isnrm2  18803  cmpfi  18852  bwthOLD  18855  1stcfb  18890  1stccnp  18907  ptrescn  19053  txkgen  19066  xkoinjcn  19101  trfil3  19302  fmid  19374  lmflf  19419  txflf  19420  ptcmplem3  19467  tsmsf1o  19560  ucnprima  19698  metrest  19940  metcnp  19957  metcnp2  19958  txmetcnp  19963  metuel2  19995  metustblOLD  19996  metustbl  19997  metutopOLD  19998  psmetutop  19999  metucnOLD  20004  metucn  20005  evth2  20373  lmmbrf  20614  iscfil2  20618  fmcfil  20624  iscau2  20629  iscau4  20631  iscauf  20632  caucfil  20635  iscmet3lem3  20642  cfilresi  20647  causs  20650  lmclim  20654  ivth2  20780  ovolfioo  20792  ovolficc  20793  ovolshftlem1  20833  ovolscalem1  20837  volsup2  20926  ismbf3d  20973  mbfaddlem  20979  mbfsup  20983  mbfinf  20984  itg2seq  21061  itg2gt0  21079  ellimc2  21193  ellimc3  21195  rolle  21303  cmvth  21304  mvth  21305  dvlip  21306  dvivth  21323  lhop1lem  21326  deg1ldg  21447  ulm2  21734  ulmdvlem3  21751  dcubic  22125  mcubic  22126  cubic2  22127  rlimcnp  22243  ftalem3  22296  isppw2  22337  lgsquadlem2  22578  dchrmusumlema  22626  dchrisum0lema  22647  tglowdim2l  22918  mirreu3  22923  axsegcon  22995  axpasch  23009  axcontlem7  23038  nmobndi  23997  nmounbi  23998  nmoo0  24013  h2hcau  24203  h2hlm  24204  shsel3  24540  pjhtheu2  24641  chscllem2  24863  adjbdln  25309  branmfn  25331  pjimai  25402  chrelati  25590  cdj3lem3  25664  cdj3lem3b  25666  dfimafnf  25773  ofpreima  25807  isarchi2  26025  submarchi  26026  archirng  26028  archiabl  26038  gsumpropd2lem  26092  isarchiofld  26137  lmdvg  26236  esumfsup  26372  dya2icoseg2  26546  eulerpartlemgh  26608  ballotlemodife  26727  ballotlemsima  26745  erdszelem10  26935  iscvm  26995  prodeq2ii  27272  zprod  27296  wsuclem  27608  seglelin  27993  outsideofeu  28008  supadd  28259  ptrest  28266  mblfinlem1  28269  opnrebl  28356  opnrebl2  28357  filnetlem4  28443  lmclim2  28495  caures  28497  isbnd3b  28525  heiborlem7  28557  heiborlem10  28560  rrncmslem  28572  isdrngo2  28605  prter3  28869  elrfirn  28873  elrfirn2  28874  mrefg3  28886  diophin  28953  diophun  28954  diophren  28994  rmxycomplete  29100  wepwsolem  29236  fnwe2lem2  29246  islssfg  29265  dfaimafn  29914  usgra2pth0  30145  el2spthonot0  30233  usg2spthonot1  30252  clwwlkfo  30302  eclclwwlkn1  30349  rusgranumwlks  30417  usgreg2spot  30503  bj-finsumval0  32156  islshpsm  32195  lsatfixedN  32224  lrelat  32229  eqlkr2  32315  lshpkrlem1  32325  lfl1dim  32336  eqlkr4  32380  ishlat3N  32569  hlsupr2  32601  hlrelat5N  32615  hlrelat  32616  cvrval5  32629  cvrat42  32658  athgt  32670  3dim0  32671  islln3  32724  llnexatN  32735  islpln3  32747  islvol3  32790  islvol5  32793  isline4N  32991  polval2N  33120  4atex3  33295  cdleme0ex2N  33438  cdlemefrs29cpre1  33612  cdlemb3  33820  cdlemg33c  33922  cdlemg33e  33924  dia1dim2  34277  cdlemm10N  34333  dib1dim2  34383  diclspsn  34409  dih1dimatlem  34544  dihatexv2  34554  djhcvat42  34630  dihjat1lem  34643  dvh4dimat  34653  dvh2dimatN  34655  lcfrlem9  34765  mapdval4N  34847  mapdcv  34875