Theorem rexbidva 2915

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

Syntax hints:   -> wi 4   <-> wb 184   /\ wa 367   e. wcel 1842   E.wrex 2755

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725

This theorem depends on definitions:  df-bi 185  df-an 369  df-ex 1634  df-rex 2760

This theorem is referenced by:  rexbidv  2918  2rexbiia  2923  2rexbidva  2924  rexeqbidva  3021  frinxp  4889  onfr  5449  dfimafn  5898  funimass4  5900  fconstfvOLD  6115  fliftel  6190  fliftf  6196  isomin  6216  f1oiso  6230  releldm2  6834  oaass  7247  qsinxp  7424  qliftel  7431  fimaxg  7801  ordunifi  7804  supisolem  7965  wemapwe  8171  wemapweOLD  8172  cflim2  8675  cfsmolem  8682  alephsing  8688  brdom7disj  8941  brdom6disj  8942  alephreg  8989  nqereu  9337  1idpr  9437  map2psrpr  9517  axsup  9691  rereccl  10303  sup3  10540  infm3  10542  creur  10570  creui  10571  nndiv  10617  nnrecl  10834  rpnnen1lem1  11253  rpnnen1lem2  11254  rpnnen1lem3  11255  rpnnen1lem5  11257  supxrbnd1  11566  supxrbnd2  11567  supxrbnd  11573  rabssnn0fi  12136  mptnn0fsupp  12147  expnlbnd  12340  limsuplt  13451  clim2  13476  clim2c  13477  clim0c  13479  ello12  13488  elo12  13499  rlimresb  13537  climabs0  13557  sumeq2ii  13664  mertens  13847  prodeq2ii  13872  zprod  13896  alzdvds  14245  oddm1even  14256  divalglem4  14263  divalgb  14271  modprmn0modprm0  14541  vdwlem6  14713  vdwlem11  14718  vdw  14721  ramval  14735  imasleval  15155  dfiso3  15386  fullestrcsetc  15744  fullsetcestrc  15759  isipodrs  16115  ipodrsfi  16117  gsumpropd2lem  16224  mndpropd  16270  grppropd  16392  conjnmzb  16625  symgextfo  16771  symgfixfo  16788  sylow1lem2  16943  sylow3lem1  16971  sylow3lem3  16973  lsmelvalm  16995  lsmass  17012  iscyg3  17213  ghmcyg  17222  cycsubgcyg  17227  pgpfac1lem2  17446  pgpfac1lem4  17449  ablfac2  17460  dvdsr02  17625  crngunit  17631  dvdsrpropd  17665  lpigen  18224  znunit  18900  elfilspd  19130  scmatmats  19305  symgmatr01  19448  isclo  19881  iscnp3  20038  lmbrf  20054  cncnp  20074  lmss  20092  isnrm2  20152  cmpfi  20201  1stcfb  20238  1stccnp  20255  ptrescn  20432  txkgen  20445  xkoinjcn  20480  trfil3  20681  fmid  20753  lmflf  20798  txflf  20799  ptcmplem3  20846  tsmsf1o  20939  ucnprima  21077  metrest  21319  metcnp  21336  metcnp2  21337  txmetcnp  21342  metuel2  21374  metustblOLD  21375  metustbl  21376  metutopOLD  21377  psmetutop  21378  metucnOLD  21383  metucn  21384  evth2  21752  lmmbrf  21993  iscfil2  21997  fmcfil  22003  iscau2  22008  iscau4  22010  iscauf  22011  caucfil  22014  iscmet3lem3  22021  cfilresi  22026  causs  22029  lmclim  22033  ivth2  22159  ovolfioo  22171  ovolficc  22172  ovolshftlem1  22212  ovolscalem1  22216  volsup2  22306  ismbf3d  22353  mbfaddlem  22359  mbfsup  22363  mbfinf  22364  itg2seq  22441  itg2gt0  22459  ellimc2  22573  ellimc3  22575  rolle  22683  cmvth  22684  mvth  22685  dvlip  22686  dvivth  22703  lhop1lem  22706  deg1ldg  22784  ulm2  23072  ulmdvlem3  23089  dcubic  23502  mcubic  23503  cubic2  23504  rlimcnp  23621  ftalem3  23729  isppw2  23770  lgsquadlem2  24011  dchrmusumlema  24059  dchrisum0lema  24080  tglowdim2l  24416  mirreu3  24420  oppcom  24503  axsegcon  24647  axpasch  24661  axcontlem7  24690  clwwlkfo  25214  eclclwwlkn1  25249  el2spthonot0  25288  usg2spthonot1  25307  rusgranumwlks  25373  usgreg2spot  25484  nmobndi  26104  nmounbi  26105  nmoo0  26120  h2hcau  26310  h2hlm  26311  shsel3  26647  pjhtheu2  26748  chscllem2  26970  adjbdln  27415  branmfn  27437  pjimai  27508  chrelati  27696  cdj3lem3  27770  cdj3lem3b  27772  dfimafnf  27916  ofpreima  27950  isarchi2  28181  submarchi  28182  archirng  28184  archiabl  28194  isarchiofld  28260  ordtconlem1  28359  lmdvg  28388  esumfsup  28517  dya2icoseg2  28726  eulerpartlemgh  28823  ballotlemodife  28942  ballotlemsima  28960  erdszelem10  29497  iscvm  29556  wsuclem  30081  seglelin  30454  outsideofeu  30469  opnrebl  30548  opnrebl2  30549  filnetlem4  30609  bj-finsumval0  31227  supadd  31414  ptrest  31420  mblfinlem1  31423  lmclim2  31533  caures  31535  isbnd3b  31563  heiborlem7  31595  heiborlem10  31598  rrncmslem  31610  isdrngo2  31643  prter3  31905  islshpsm  31998  lsatfixedN  32027  lrelat  32032  eqlkr2  32118  lshpkrlem1  32128  lfl1dim  32139  eqlkr4  32183  ishlat3N  32372  hlsupr2  32404  hlrelat5N  32418  hlrelat  32419  cvrval5  32432  cvrat42  32461  athgt  32473  3dim0  32474  islln3  32527  llnexatN  32538  islpln3  32550  islvol3  32593  islvol5  32596  isline4N  32794  polval2N  32923  4atex3  33098  cdleme0ex2N  33242  cdlemefrs29cpre1  33417  cdlemb3  33625  cdlemg33c  33727  cdlemg33e  33729  dia1dim2  34082  cdlemm10N  34138  dib1dim2  34188  diclspsn  34214  dih1dimatlem  34349  dihatexv2  34359  djhcvat42  34435  dihjat1lem  34448  dvh4dimat  34458  dvh2dimatN  34460  lcfrlem9  34570  mapdval4N  34652  mapdcv  34680  elrfirn  34989  elrfirn2  34990  mrefg3  35002  diophin  35067  diophun  35068  diophren  35108  rmxycomplete  35214  wepwsolem  35349  fnwe2lem2  35359  islssfg  35378  extoimad  35992  evthiccabs  36898  clim2f  37010  clim2cf  37024  clim0cf  37028  fourierdlem73  37330  fourierdlem83  37340  dfaimafn  37618  iccelpart  37700  dfeven2  37732  dfodd3  37733  usgra2pth0  37984  elbigo2  38683