Theorem rexbidva 2889

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 653	. 2 |- ( ph -> ( ( x e. A /\ ps ) <-> ( x e. A /\ ch ) ) )
3	2	rexbidv2 2888	1 |- ( ph -> ( E. x e. A ps <-> E. x e. A ch ) )

Syntax hints:   -> wi 4   <-> wb 189   /\ wa 376   e. wcel 1904   E.wrex 2757

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766

This theorem depends on definitions:  df-bi 190  df-an 378  df-ex 1672  df-rex 2762

This theorem is referenced by:  rexbidv  2892  2rexbiia  2895  2rexbidva  2896  rexeqbidva  2990  frinxp  4905  onfr  5469  dfimafn  5928  funimass4  5930  fliftel  6220  fliftf  6226  isomin  6246  f1oiso  6260  releldm2  6862  oaass  7280  qsinxp  7457  qliftel  7464  fimaxg  7836  ordunifi  7839  supisolem  8007  fiming  8032  wemapwe  8220  cflim2  8711  cfsmolem  8718  alephsing  8724  brdom7disj  8977  brdom6disj  8978  alephreg  9025  nqereu  9372  1idpr  9472  map2psrpr  9552  axsup  9727  rereccl  10347  sup3  10588  infm3  10590  supadd  10597  creur  10625  creui  10626  nndiv  10672  nnrecl  10891  rpnnen1lem1  11313  rpnnen1lem2  11314  rpnnen1lem3  11315  rpnnen1lem5  11317  supxrbnd1  11632  supxrbnd2  11633  supxrbnd  11639  rabssnn0fi  12236  mptnn0fsupp  12247  expnlbnd  12440  limsuplt  13615  limsupltOLD  13616  clim2  13645  clim2c  13646  clim0c  13648  ello12  13657  elo12  13668  rlimresb  13706  climabs0  13726  sumeq2ii  13836  mertens  14019  prodeq2ii  14044  zprod  14068  alzdvds  14432  oddm1even  14444  divalglem4  14454  divalgb  14464  modprmn0modprm0  14837  vdwlem6  15015  vdwlem11  15020  vdw  15023  ramval  15039  ramvalOLD  15040  imasleval  15525  dfiso3  15756  fullestrcsetc  16114  fullsetcestrc  16129  isipodrs  16485  ipodrsfi  16487  gsumpropd2lem  16594  mndpropd  16640  grppropd  16762  conjnmzb  16995  symgextfo  17141  symgfixfo  17158  sylow1lem2  17329  sylow3lem1  17357  sylow3lem3  17359  lsmelvalm  17381  lsmass  17398  iscyg3  17599  ghmcyg  17608  cycsubgcyg  17613  pgpfac1lem2  17786  pgpfac1lem4  17789  ablfac2  17800  dvdsr02  17962  crngunit  17968  dvdsrpropd  18002  lpigen  18557  znunit  19211  elfilspd  19438  scmatmats  19613  symgmatr01  19756  isclo  20180  iscnp3  20337  lmbrf  20353  cncnp  20373  lmss  20391  isnrm2  20451  cmpfi  20500  1stcfb  20537  1stccnp  20554  ptrescn  20731  txkgen  20744  xkoinjcn  20779  trfil3  20981  fmid  21053  lmflf  21098  txflf  21099  ptcmplem3  21147  tsmsf1o  21237  ucnprima  21375  metrest  21617  metcnp  21634  metcnp2  21635  txmetcnp  21640  metuel2  21658  metustbl  21659  psmetutop  21660  metucn  21664  evth2  22066  lmmbrf  22310  iscfil2  22314  fmcfil  22320  iscau2  22325  iscau4  22327  iscauf  22328  caucfil  22331  iscmet3lem3  22338  cfilresi  22343  causs  22346  lmclim  22350  ivth2  22484  ovolfioo  22498  ovolficc  22499  ovolshftlem1  22540  ovolscalem1  22544  volsup2  22642  ismbf3d  22689  mbfaddlem  22695  mbfsup  22699  mbfinf  22700  mbfinfOLD  22701  itg2seq  22779  itg2gt0  22797  ellimc2  22911  ellimc3  22913  rolle  23021  cmvth  23022  mvth  23023  dvlip  23024  dvivth  23041  lhop1lem  23044  deg1ldg  23120  ulm2  23419  ulmdvlem3  23436  dcubic  23851  mcubic  23852  cubic2  23853  rlimcnp  23970  ftalem3  24078  isppw2  24121  lgsquadlem2  24362  dchrmusumlema  24410  dchrisum0lema  24431  tglowdim2l  24774  mirreu3  24778  oppcom  24865  iscgra1  24931  axsegcon  25036  axpasch  25050  axcontlem7  25079  clwwlkfo  25604  eclclwwlkn1  25639  el2spthonot0  25678  usg2spthonot1  25697  rusgranumwlks  25763  usgreg2spot  25874  nmobndi  26497  nmounbi  26498  nmoo0  26513  h2hcau  26713  h2hlm  26714  shsel3  27049  pjhtheu2  27150  chscllem2  27372  adjbdln  27817  branmfn  27839  pjimai  27910  chrelati  28098  cdj3lem3  28172  cdj3lem3b  28174  dfimafnf  28309  ofpreima  28343  isarchi2  28576  submarchi  28577  archirng  28579  archiabl  28589  isarchiofld  28654  ordtconlem1  28804  lmdvg  28833  esumfsup  28965  dya2icoseg2  29173  eulerpartlemgh  29284  ballotlemodife  29403  ballotlemsima  29421  ballotlemsimaOLD  29459  erdszelem10  29995  iscvm  30054  wsuclem  30579  seglelin  30954  outsideofeu  30969  opnrebl  31047  opnrebl2  31048  filnetlem4  31108  bj-finsumval0  31772  phpreu  31993  ptrest  32003  poimirlem3  32007  poimirlem4  32008  poimirlem17  32021  poimirlem26  32030  poimirlem27  32031  broucube  32038  mblfinlem1  32041  lmclim2  32151  caures  32153  isbnd3b  32181  heiborlem7  32213  heiborlem10  32216  rrncmslem  32228  isdrngo2  32261  prter3  32518  islshpsm  32617  lsatfixedN  32646  lrelat  32651  eqlkr2  32737  lshpkrlem1  32747  lfl1dim  32758  eqlkr4  32802  ishlat3N  32991  hlsupr2  33023  hlrelat5N  33037  hlrelat  33038  cvrval5  33051  cvrat42  33080  athgt  33092  3dim0  33093  islln3  33146  llnexatN  33157  islpln3  33169  islvol3  33212  islvol5  33215  isline4N  33413  polval2N  33542  4atex3  33717  cdleme0ex2N  33861  cdlemefrs29cpre1  34036  cdlemb3  34244  cdlemg33c  34346  cdlemg33e  34348  dia1dim2  34701  cdlemm10N  34757  dib1dim2  34807  diclspsn  34833  dih1dimatlem  34968  dihatexv2  34978  djhcvat42  35054  dihjat1lem  35067  dvh4dimat  35077  dvh2dimatN  35079  lcfrlem9  35189  mapdval4N  35271  mapdcv  35299  elrfirn  35608  elrfirn2  35609  mrefg3  35621  diophin  35686  diophun  35687  diophren  35727  rmxycomplete  35836  wepwsolem  35971  fnwe2lem2  35980  islssfg  35999  extoimad  36678  supsubc  37663  infxrbnd2  37679  evthiccabs  37689  elicores  37731  clim2f  37813  clim2cf  37828  clim0cf  37832  fourierdlem73  38155  fourierdlem83  38165  ovolval2  38584  dfaimafn  38812  iccelpart  38892  dfeven2  38924  dfodd3  38925  eucrctshift  40155  usgra2pth0  40177  elbigo2  40871