Theorem rexbidva 2949

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689

This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1598  df-rex 2797

This theorem is referenced by:  rexbidv  2952  2rexbiia  2957  2rexbidva  2958  rexeqbidva  3055  onfr  4903  frinxp  5051  dfimafn  5903  funimass4  5905  fconstfvOLD  6114  fliftel  6188  fliftf  6194  isomin  6214  f1oiso  6228  releldm2  6831  oaass  7208  qsinxp  7385  qliftel  7392  fimaxg  7765  ordunifi  7768  supisolem  7929  wemapwe  8137  wemapweOLD  8138  cflim2  8641  cfsmolem  8648  alephsing  8654  brdom7disj  8907  brdom6disj  8908  alephreg  8955  nqereu  9305  1idpr  9405  map2psrpr  9485  axsup  9658  rereccl  10263  sup3  10501  infm3  10503  creur  10531  creui  10532  nndiv  10577  nnrecl  10794  rpnnen1lem1  11212  rpnnen1lem2  11213  rpnnen1lem3  11214  rpnnen1lem5  11216  supxrbnd1  11517  supxrbnd2  11518  supxrbnd  11524  rabssnn0fi  12069  mptnn0fsupp  12077  expnlbnd  12270  limsuplt  13276  clim2  13301  clim2c  13302  clim0c  13304  ello12  13313  elo12  13324  rlimresb  13362  climabs0  13382  sumeq2ii  13489  mertens  13669  alzdvds  13908  oddm1even  13919  divalglem4  13926  divalgb  13934  modprmn0modprm0  14204  vdwlem6  14376  vdwlem11  14381  vdw  14384  ramval  14398  imasleval  14810  isipodrs  15660  ipodrsfi  15662  gsumpropd2lem  15769  mndpropd  15815  grppropd  15937  conjnmzb  16170  symgextfo  16316  symgfixfo  16333  sylow1lem2  16488  sylow3lem1  16516  sylow3lem3  16518  lsmelvalm  16540  lsmass  16557  iscyg3  16758  ghmcyg  16767  cycsubgcyg  16772  pgpfac1lem2  16994  pgpfac1lem4  16997  ablfac2  17008  dvdsr02  17173  crngunit  17179  dvdsrpropd  17213  lpigen  17772  znunit  18469  elfilspd  18705  scmatmats  18880  symgmatr01  19023  isclo  19454  iscnp3  19611  lmbrf  19627  cncnp  19647  lmss  19665  isnrm2  19725  cmpfi  19774  bwthOLD  19777  1stcfb  19812  1stccnp  19829  ptrescn  20006  txkgen  20019  xkoinjcn  20054  trfil3  20255  fmid  20327  lmflf  20372  txflf  20373  ptcmplem3  20420  tsmsf1o  20513  ucnprima  20651  metrest  20893  metcnp  20910  metcnp2  20911  txmetcnp  20916  metuel2  20948  metustblOLD  20949  metustbl  20950  metutopOLD  20951  psmetutop  20952  metucnOLD  20957  metucn  20958  evth2  21326  lmmbrf  21567  iscfil2  21571  fmcfil  21577  iscau2  21582  iscau4  21584  iscauf  21585  caucfil  21588  iscmet3lem3  21595  cfilresi  21600  causs  21603  lmclim  21607  ivth2  21733  ovolfioo  21745  ovolficc  21746  ovolshftlem1  21786  ovolscalem1  21790  volsup2  21880  ismbf3d  21927  mbfaddlem  21933  mbfsup  21937  mbfinf  21938  itg2seq  22015  itg2gt0  22033  ellimc2  22147  ellimc3  22149  rolle  22257  cmvth  22258  mvth  22259  dvlip  22260  dvivth  22277  lhop1lem  22280  deg1ldg  22358  ulm2  22645  ulmdvlem3  22662  dcubic  23042  mcubic  23043  cubic2  23044  rlimcnp  23160  ftalem3  23213  isppw2  23254  lgsquadlem2  23495  dchrmusumlema  23543  dchrisum0lema  23564  tglowdim2l  23896  mirreu3  23900  oppcom  23981  axsegcon  24095  axpasch  24109  axcontlem7  24138  clwwlkfo  24662  eclclwwlkn1  24697  el2spthonot0  24736  usg2spthonot1  24755  rusgranumwlks  24821  usgreg2spot  24932  nmobndi  25555  nmounbi  25556  nmoo0  25571  h2hcau  25761  h2hlm  25762  shsel3  26098  pjhtheu2  26199  chscllem2  26421  adjbdln  26867  branmfn  26889  pjimai  26960  chrelati  27148  cdj3lem3  27222  cdj3lem3b  27224  dfimafnf  27338  ofpreima  27372  isarchi2  27595  submarchi  27596  archirng  27598  archiabl  27608  isarchiofld  27673  ordtconlem1  27772  lmdvg  27801  esumfsup  27942  dya2icoseg2  28115  eulerpartlemgh  28183  ballotlemodife  28302  ballotlemsima  28320  erdszelem10  28510  iscvm  28570  prodeq2ii  29013  zprod  29037  wsuclem  29349  seglelin  29734  outsideofeu  29749  supadd  30010  ptrest  30016  mblfinlem1  30019  opnrebl  30106  opnrebl2  30107  filnetlem4  30167  lmclim2  30219  caures  30221  isbnd3b  30249  heiborlem7  30281  heiborlem10  30284  rrncmslem  30296  isdrngo2  30329  prter3  30591  elrfirn  30595  elrfirn2  30596  mrefg3  30608  diophin  30674  diophun  30675  diophren  30715  rmxycomplete  30821  wepwsolem  30955  fnwe2lem2  30965  islssfg  30984  evthiccabs  31461  clim2f  31546  clim2cf  31560  clim0cf  31564  fourierdlem73  31847  fourierdlem83  31857  dfaimafn  32084  usgra2pth0  32189  bj-finsumval0  34365  islshpsm  34407  lsatfixedN  34436  lrelat  34441  eqlkr2  34527  lshpkrlem1  34537  lfl1dim  34548  eqlkr4  34592  ishlat3N  34781  hlsupr2  34813  hlrelat5N  34827  hlrelat  34828  cvrval5  34841  cvrat42  34870  athgt  34882  3dim0  34883  islln3  34936  llnexatN  34947  islpln3  34959  islvol3  35002  islvol5  35005  isline4N  35203  polval2N  35332  4atex3  35507  cdleme0ex2N  35651  cdlemefrs29cpre1  35826  cdlemb3  36034  cdlemg33c  36136  cdlemg33e  36138  dia1dim2  36491  cdlemm10N  36547  dib1dim2  36597  diclspsn  36623  dih1dimatlem  36758  dihatexv2  36768  djhcvat42  36844  dihjat1lem  36857  dvh4dimat  36867  dvh2dimatN  36869  lcfrlem9  36979  mapdval4N  37061  mapdcv  37089  extoimad  37586