Theorem rexbidva 2936

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

Syntax hints:   -> wi 4   <-> wb 187   /\ wa 370   e. wcel 1868   E.wrex 2776

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748

This theorem depends on definitions:  df-bi 188  df-an 372  df-ex 1660  df-rex 2781

This theorem is referenced by:  rexbidv  2939  2rexbiia  2944  2rexbidva  2945  rexeqbidva  3042  frinxp  4916  onfr  5478  dfimafn  5927  funimass4  5929  fconstfvOLD  6139  fliftel  6214  fliftf  6220  isomin  6240  f1oiso  6254  releldm2  6854  oaass  7267  qsinxp  7444  qliftel  7451  fimaxg  7821  ordunifi  7824  supisolem  7992  fiming  8017  wemapwe  8204  cflim2  8694  cfsmolem  8701  alephsing  8707  brdom7disj  8960  brdom6disj  8961  alephreg  9008  nqereu  9355  1idpr  9455  map2psrpr  9535  axsup  9710  rereccl  10326  sup3  10567  infm3  10569  supadd  10576  creur  10604  creui  10605  nndiv  10651  nnrecl  10868  rpnnen1lem1  11291  rpnnen1lem2  11292  rpnnen1lem3  11293  rpnnen1lem5  11295  supxrbnd1  11608  supxrbnd2  11609  supxrbnd  11615  rabssnn0fi  12198  mptnn0fsupp  12209  expnlbnd  12402  limsuplt  13526  limsupltOLD  13527  clim2  13556  clim2c  13557  clim0c  13559  ello12  13568  elo12  13579  rlimresb  13617  climabs0  13637  sumeq2ii  13747  mertens  13930  prodeq2ii  13955  zprod  13979  alzdvds  14343  oddm1even  14354  divalglem4  14363  divalgb  14373  modprmn0modprm0  14746  vdwlem6  14924  vdwlem11  14929  vdw  14932  ramval  14948  ramvalOLD  14949  imasleval  15435  dfiso3  15666  fullestrcsetc  16024  fullsetcestrc  16039  isipodrs  16395  ipodrsfi  16397  gsumpropd2lem  16504  mndpropd  16550  grppropd  16672  conjnmzb  16905  symgextfo  17051  symgfixfo  17068  sylow1lem2  17239  sylow3lem1  17267  sylow3lem3  17269  lsmelvalm  17291  lsmass  17308  iscyg3  17509  ghmcyg  17518  cycsubgcyg  17523  pgpfac1lem2  17696  pgpfac1lem4  17699  ablfac2  17710  dvdsr02  17872  crngunit  17878  dvdsrpropd  17912  lpigen  18468  znunit  19121  elfilspd  19348  scmatmats  19523  symgmatr01  19666  isclo  20090  iscnp3  20247  lmbrf  20263  cncnp  20283  lmss  20301  isnrm2  20361  cmpfi  20410  1stcfb  20447  1stccnp  20464  ptrescn  20641  txkgen  20654  xkoinjcn  20689  trfil3  20890  fmid  20962  lmflf  21007  txflf  21008  ptcmplem3  21056  tsmsf1o  21146  ucnprima  21284  metrest  21526  metcnp  21543  metcnp2  21544  txmetcnp  21549  metuel2  21567  metustbl  21568  psmetutop  21569  metucn  21573  evth2  21975  lmmbrf  22219  iscfil2  22223  fmcfil  22229  iscau2  22234  iscau4  22236  iscauf  22237  caucfil  22240  iscmet3lem3  22247  cfilresi  22252  causs  22255  lmclim  22259  ivth2  22393  ovolfioo  22407  ovolficc  22408  ovolshftlem1  22449  ovolscalem1  22453  volsup2  22550  ismbf3d  22597  mbfaddlem  22603  mbfsup  22607  mbfinf  22608  mbfinfOLD  22609  itg2seq  22687  itg2gt0  22705  ellimc2  22819  ellimc3  22821  rolle  22929  cmvth  22930  mvth  22931  dvlip  22932  dvivth  22949  lhop1lem  22952  deg1ldg  23028  ulm2  23327  ulmdvlem3  23344  dcubic  23759  mcubic  23760  cubic2  23761  rlimcnp  23878  ftalem3  23986  isppw2  24029  lgsquadlem2  24270  dchrmusumlema  24318  dchrisum0lema  24339  tglowdim2l  24682  mirreu3  24686  oppcom  24773  iscgra1  24839  axsegcon  24944  axpasch  24958  axcontlem7  24987  clwwlkfo  25511  eclclwwlkn1  25546  el2spthonot0  25585  usg2spthonot1  25604  rusgranumwlks  25670  usgreg2spot  25781  nmobndi  26402  nmounbi  26403  nmoo0  26418  h2hcau  26618  h2hlm  26619  shsel3  26954  pjhtheu2  27055  chscllem2  27277  adjbdln  27722  branmfn  27744  pjimai  27815  chrelati  28003  cdj3lem3  28077  cdj3lem3b  28079  dfimafnf  28223  ofpreima  28258  isarchi2  28497  submarchi  28498  archirng  28500  archiabl  28510  isarchiofld  28576  ordtconlem1  28726  lmdvg  28755  esumfsup  28887  dya2icoseg2  29096  eulerpartlemgh  29207  ballotlemodife  29326  ballotlemsima  29344  ballotlemsimaOLD  29382  erdszelem10  29919  iscvm  29978  wsuclem  30503  seglelin  30876  outsideofeu  30891  opnrebl  30969  opnrebl2  30970  filnetlem4  31030  bj-finsumval0  31654  phpreu  31843  ptrest  31853  poimirlem3  31857  poimirlem4  31858  poimirlem17  31871  poimirlem26  31880  poimirlem27  31881  broucube  31888  mblfinlem1  31891  lmclim2  32001  caures  32003  isbnd3b  32031  heiborlem7  32063  heiborlem10  32066  rrncmslem  32078  isdrngo2  32111  prter3  32372  islshpsm  32465  lsatfixedN  32494  lrelat  32499  eqlkr2  32585  lshpkrlem1  32595  lfl1dim  32606  eqlkr4  32650  ishlat3N  32839  hlsupr2  32871  hlrelat5N  32885  hlrelat  32886  cvrval5  32899  cvrat42  32928  athgt  32940  3dim0  32941  islln3  32994  llnexatN  33005  islpln3  33017  islvol3  33060  islvol5  33063  isline4N  33261  polval2N  33390  4atex3  33565  cdleme0ex2N  33709  cdlemefrs29cpre1  33884  cdlemb3  34092  cdlemg33c  34194  cdlemg33e  34196  dia1dim2  34549  cdlemm10N  34605  dib1dim2  34655  diclspsn  34681  dih1dimatlem  34816  dihatexv2  34826  djhcvat42  34902  dihjat1lem  34915  dvh4dimat  34925  dvh2dimatN  34927  lcfrlem9  35037  mapdval4N  35119  mapdcv  35147  elrfirn  35456  elrfirn2  35457  mrefg3  35469  diophin  35534  diophun  35535  diophren  35575  rmxycomplete  35685  wepwsolem  35820  fnwe2lem2  35829  islssfg  35848  extoimad  36465  evthiccabs  37424  elicores  37465  clim2f  37536  clim2cf  37551  clim0cf  37555  fourierdlem73  37863  fourierdlem83  37873  dfaimafn  38379  iccelpart  38459  dfeven2  38491  dfodd3  38492  usgra2pth0  38941  elbigo2  39637