Theorem rexbidva 2898

Description: Formula-building rule for restricted existential quantifier (deduction rule). (Contributed by NM, 9-Mar-1997.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 6-Dec-2019.) (Proof shortened by Wolf Lammen, 10-Dec-2019.)

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		rexbidva.1	. . 3 |- ( ( ph /\ x e. A ) -> ( ps <-> ch ) )
2	1	pm5.32da 647	. 2 |- ( ph -> ( ( x e. A /\ ps ) <-> ( x e. A /\ ch ) ) )
3	2	rexbidv2 2897	1 |- ( ph -> ( E. x e. A ps <-> E. x e. A ch ) )

Syntax hints:   -> wi 4   <-> wb 188   /\ wa 371   e. wcel 1887   E.wrex 2738

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758

This theorem depends on definitions:  df-bi 189  df-an 373  df-ex 1664  df-rex 2743

This theorem is referenced by:  rexbidv  2901  2rexbiia  2906  2rexbidva  2907  rexeqbidva  3004  frinxp  4900  onfr  5462  dfimafn  5914  funimass4  5916  fconstfvOLD  6127  fliftel  6202  fliftf  6208  isomin  6228  f1oiso  6242  releldm2  6843  oaass  7262  qsinxp  7439  qliftel  7446  fimaxg  7818  ordunifi  7821  supisolem  7989  fiming  8014  wemapwe  8202  cflim2  8693  cfsmolem  8700  alephsing  8706  brdom7disj  8959  brdom6disj  8960  alephreg  9007  nqereu  9354  1idpr  9454  map2psrpr  9534  axsup  9709  rereccl  10325  sup3  10566  infm3  10568  supadd  10575  creur  10603  creui  10604  nndiv  10650  nnrecl  10867  rpnnen1lem1  11290  rpnnen1lem2  11291  rpnnen1lem3  11292  rpnnen1lem5  11294  supxrbnd1  11607  supxrbnd2  11608  supxrbnd  11614  rabssnn0fi  12198  mptnn0fsupp  12209  expnlbnd  12402  limsuplt  13538  limsupltOLD  13539  clim2  13568  clim2c  13569  clim0c  13571  ello12  13580  elo12  13591  rlimresb  13629  climabs0  13649  sumeq2ii  13759  mertens  13942  prodeq2ii  13967  zprod  13991  alzdvds  14355  oddm1even  14366  divalglem4  14375  divalgb  14385  modprmn0modprm0  14758  vdwlem6  14936  vdwlem11  14941  vdw  14944  ramval  14960  ramvalOLD  14961  imasleval  15447  dfiso3  15678  fullestrcsetc  16036  fullsetcestrc  16051  isipodrs  16407  ipodrsfi  16409  gsumpropd2lem  16516  mndpropd  16562  grppropd  16684  conjnmzb  16917  symgextfo  17063  symgfixfo  17080  sylow1lem2  17251  sylow3lem1  17279  sylow3lem3  17281  lsmelvalm  17303  lsmass  17320  iscyg3  17521  ghmcyg  17530  cycsubgcyg  17535  pgpfac1lem2  17708  pgpfac1lem4  17711  ablfac2  17722  dvdsr02  17884  crngunit  17890  dvdsrpropd  17924  lpigen  18480  znunit  19134  elfilspd  19361  scmatmats  19536  symgmatr01  19679  isclo  20103  iscnp3  20260  lmbrf  20276  cncnp  20296  lmss  20314  isnrm2  20374  cmpfi  20423  1stcfb  20460  1stccnp  20477  ptrescn  20654  txkgen  20667  xkoinjcn  20702  trfil3  20903  fmid  20975  lmflf  21020  txflf  21021  ptcmplem3  21069  tsmsf1o  21159  ucnprima  21297  metrest  21539  metcnp  21556  metcnp2  21557  txmetcnp  21562  metuel2  21580  metustbl  21581  psmetutop  21582  metucn  21586  evth2  21988  lmmbrf  22232  iscfil2  22236  fmcfil  22242  iscau2  22247  iscau4  22249  iscauf  22250  caucfil  22253  iscmet3lem3  22260  cfilresi  22265  causs  22268  lmclim  22272  ivth2  22406  ovolfioo  22420  ovolficc  22421  ovolshftlem1  22462  ovolscalem1  22466  volsup2  22563  ismbf3d  22610  mbfaddlem  22616  mbfsup  22620  mbfinf  22621  mbfinfOLD  22622  itg2seq  22700  itg2gt0  22718  ellimc2  22832  ellimc3  22834  rolle  22942  cmvth  22943  mvth  22944  dvlip  22945  dvivth  22962  lhop1lem  22965  deg1ldg  23041  ulm2  23340  ulmdvlem3  23357  dcubic  23772  mcubic  23773  cubic2  23774  rlimcnp  23891  ftalem3  23999  isppw2  24042  lgsquadlem2  24283  dchrmusumlema  24331  dchrisum0lema  24352  tglowdim2l  24695  mirreu3  24699  oppcom  24786  iscgra1  24852  axsegcon  24957  axpasch  24971  axcontlem7  25000  clwwlkfo  25525  eclclwwlkn1  25560  el2spthonot0  25599  usg2spthonot1  25618  rusgranumwlks  25684  usgreg2spot  25795  nmobndi  26416  nmounbi  26417  nmoo0  26432  h2hcau  26632  h2hlm  26633  shsel3  26968  pjhtheu2  27069  chscllem2  27291  adjbdln  27736  branmfn  27758  pjimai  27829  chrelati  28017  cdj3lem3  28091  cdj3lem3b  28093  dfimafnf  28233  ofpreima  28268  isarchi2  28502  submarchi  28503  archirng  28505  archiabl  28515  isarchiofld  28580  ordtconlem1  28730  lmdvg  28759  esumfsup  28891  dya2icoseg2  29100  eulerpartlemgh  29211  ballotlemodife  29330  ballotlemsima  29348  ballotlemsimaOLD  29386  erdszelem10  29923  iscvm  29982  wsuclem  30508  seglelin  30883  outsideofeu  30898  opnrebl  30976  opnrebl2  30977  filnetlem4  31037  bj-finsumval0  31702  phpreu  31929  ptrest  31939  poimirlem3  31943  poimirlem4  31944  poimirlem17  31957  poimirlem26  31966  poimirlem27  31967  broucube  31974  mblfinlem1  31977  lmclim2  32087  caures  32089  isbnd3b  32117  heiborlem7  32149  heiborlem10  32152  rrncmslem  32164  isdrngo2  32197  prter3  32454  islshpsm  32546  lsatfixedN  32575  lrelat  32580  eqlkr2  32666  lshpkrlem1  32676  lfl1dim  32687  eqlkr4  32731  ishlat3N  32920  hlsupr2  32952  hlrelat5N  32966  hlrelat  32967  cvrval5  32980  cvrat42  33009  athgt  33021  3dim0  33022  islln3  33075  llnexatN  33086  islpln3  33098  islvol3  33141  islvol5  33144  isline4N  33342  polval2N  33471  4atex3  33646  cdleme0ex2N  33790  cdlemefrs29cpre1  33965  cdlemb3  34173  cdlemg33c  34275  cdlemg33e  34277  dia1dim2  34630  cdlemm10N  34686  dib1dim2  34736  diclspsn  34762  dih1dimatlem  34897  dihatexv2  34907  djhcvat42  34983  dihjat1lem  34996  dvh4dimat  35006  dvh2dimatN  35008  lcfrlem9  35118  mapdval4N  35200  mapdcv  35228  elrfirn  35537  elrfirn2  35538  mrefg3  35550  diophin  35615  diophun  35616  diophren  35656  rmxycomplete  35765  wepwsolem  35900  fnwe2lem2  35909  islssfg  35928  extoimad  36607  supsubc  37576  evthiccabs  37593  elicores  37635  clim2f  37716  clim2cf  37731  clim0cf  37735  fourierdlem73  38043  fourierdlem83  38053  dfaimafn  38667  iccelpart  38747  dfeven2  38779  dfodd3  38780  usgra2pth0  39722  elbigo2  40416