Theorem rexbidva 2963

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 2962	1 |- ( ph -> ( E. x e. A ps <-> E. x e. A ch ) )

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675

This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1592  df-rex 2813

This theorem is referenced by:  rexbidv  2966  2rexbiia  2971  2rexbidva  2972  rexeqbidva  3068  onfr  4910  frinxp  5057  dfimafn  5907  funimass4  5909  fconstfv  6114  fliftel  6186  fliftf  6192  isomin  6212  f1oiso  6226  releldm2  6824  oaass  7200  qsinxp  7377  qliftel  7384  fimaxg  7756  ordunifi  7759  supisolem  7920  wemapwe  8128  wemapweOLD  8129  cflim2  8632  cfsmolem  8639  alephsing  8645  brdom7disj  8898  brdom6disj  8899  alephreg  8946  nqereu  9296  1idpr  9396  map2psrpr  9476  axsup  9649  rereccl  10251  sup3  10489  infm3  10491  creur  10519  creui  10520  nndiv  10565  nnrecl  10782  rpnnen1lem1  11197  rpnnen1lem2  11198  rpnnen1lem3  11199  rpnnen1lem5  11201  supxrbnd1  11502  supxrbnd2  11503  supxrbnd  11509  rabssnn0fi  12051  mptnn0fsupp  12059  expnlbnd  12251  limsuplt  13251  clim2  13276  clim2c  13277  clim0c  13279  ello12  13288  elo12  13299  rlimresb  13337  climabs0  13357  sumeq2ii  13464  mertens  13647  alzdvds  13884  oddm1even  13895  divalglem4  13902  divalgb  13910  modprmn0modprm0  14180  vdwlem6  14352  vdwlem11  14357  vdw  14360  ramval  14374  imasleval  14785  isipodrs  15637  ipodrsfi  15639  mndpropd  15752  gsumpropd2lem  15811  grppropd  15862  conjnmzb  16089  symgextfo  16235  symgfixfo  16253  sylow1lem2  16408  sylow3lem1  16436  sylow3lem3  16438  lsmelvalm  16460  lsmass  16477  iscyg3  16673  ghmcyg  16682  cycsubgcyg  16687  pgpfac1lem2  16909  pgpfac1lem4  16912  ablfac2  16923  dvdsr02  17082  crngunit  17088  dvdsrpropd  17122  lpigen  17679  znunit  18362  elfilspd  18598  scmatmats  18773  symgmatr01  18916  isclo  19347  iscnp3  19504  lmbrf  19520  cncnp  19540  lmss  19558  isnrm2  19618  cmpfi  19667  bwthOLD  19670  1stcfb  19705  1stccnp  19722  ptrescn  19868  txkgen  19881  xkoinjcn  19916  trfil3  20117  fmid  20189  lmflf  20234  txflf  20235  ptcmplem3  20282  tsmsf1o  20375  ucnprima  20513  metrest  20755  metcnp  20772  metcnp2  20773  txmetcnp  20778  metuel2  20810  metustblOLD  20811  metustbl  20812  metutopOLD  20813  psmetutop  20814  metucnOLD  20819  metucn  20820  evth2  21188  lmmbrf  21429  iscfil2  21433  fmcfil  21439  iscau2  21444  iscau4  21446  iscauf  21447  caucfil  21450  iscmet3lem3  21457  cfilresi  21462  causs  21465  lmclim  21469  ivth2  21595  ovolfioo  21607  ovolficc  21608  ovolshftlem1  21648  ovolscalem1  21652  volsup2  21742  ismbf3d  21789  mbfaddlem  21795  mbfsup  21799  mbfinf  21800  itg2seq  21877  itg2gt0  21895  ellimc2  22009  ellimc3  22011  rolle  22119  cmvth  22120  mvth  22121  dvlip  22122  dvivth  22139  lhop1lem  22142  deg1ldg  22220  ulm2  22507  ulmdvlem3  22524  dcubic  22898  mcubic  22899  cubic2  22900  rlimcnp  23016  ftalem3  23069  isppw2  23110  lgsquadlem2  23351  dchrmusumlema  23399  dchrisum0lema  23420  tglowdim2l  23737  mirreu3  23741  axsegcon  23899  axpasch  23913  axcontlem7  23942  clwwlkfo  24459  eclclwwlkn1  24494  el2spthonot0  24533  usg2spthonot1  24552  rusgranumwlks  24618  nmobndi  25216  nmounbi  25217  nmoo0  25232  h2hcau  25422  h2hlm  25423  shsel3  25759  pjhtheu2  25860  chscllem2  26082  adjbdln  26528  branmfn  26550  pjimai  26621  chrelati  26809  cdj3lem3  26883  cdj3lem3b  26885  dfimafnf  26996  ofpreima  27029  isarchi2  27241  submarchi  27242  archirng  27244  archiabl  27254  isarchiofld  27320  lmdvg  27421  esumfsup  27566  dya2icoseg2  27739  eulerpartlemgh  27807  ballotlemodife  27926  ballotlemsima  27944  erdszelem10  28134  iscvm  28194  prodeq2ii  28472  zprod  28496  wsuclem  28808  seglelin  29193  outsideofeu  29208  supadd  29469  ptrest  29476  mblfinlem1  29479  opnrebl  29566  opnrebl2  29567  filnetlem4  29653  lmclim2  29705  caures  29707  isbnd3b  29735  heiborlem7  29767  heiborlem10  29770  rrncmslem  29782  isdrngo2  29815  prter3  30078  elrfirn  30082  elrfirn2  30083  mrefg3  30095  diophin  30161  diophun  30162  diophren  30202  rmxycomplete  30308  wepwsolem  30444  fnwe2lem2  30454  islssfg  30473  evthiccabs  30912  clim2f  30997  clim2cf  31011  clim0cf  31015  fourierdlem65  31291  fourierdlem73  31299  fourierdlem83  31309  dfaimafn  31536  usgra2pth0  31643  usgreg2spot  31786  bj-finsumval0  33610  islshpsm  33652  lsatfixedN  33681  lrelat  33686  eqlkr2  33772  lshpkrlem1  33782  lfl1dim  33793  eqlkr4  33837  ishlat3N  34026  hlsupr2  34058  hlrelat5N  34072  hlrelat  34073  cvrval5  34086  cvrat42  34115  athgt  34127  3dim0  34128  islln3  34181  llnexatN  34192  islpln3  34204  islvol3  34247  islvol5  34250  isline4N  34448  polval2N  34577  4atex3  34752  cdleme0ex2N  34895  cdlemefrs29cpre1  35069  cdlemb3  35277  cdlemg33c  35379  cdlemg33e  35381  dia1dim2  35734  cdlemm10N  35790  dib1dim2  35840  diclspsn  35866  dih1dimatlem  36001  dihatexv2  36011  djhcvat42  36087  dihjat1lem  36100  dvh4dimat  36110  dvh2dimatN  36112  lcfrlem9  36222  mapdval4N  36304  mapdcv  36332