Theorem rexbidva 2965

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-5 1705

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

This theorem is referenced by:  rexbidv  2968  2rexbiia  2973  2rexbidva  2974  rexeqbidva  3071  onfr  4926  frinxp  5074  dfimafn  5922  funimass4  5924  fconstfvOLD  6135  fliftel  6208  fliftf  6214  isomin  6234  f1oiso  6248  releldm2  6849  oaass  7228  qsinxp  7405  qliftel  7412  fimaxg  7785  ordunifi  7788  supisolem  7949  wemapwe  8156  wemapweOLD  8157  cflim2  8660  cfsmolem  8667  alephsing  8673  brdom7disj  8926  brdom6disj  8927  alephreg  8974  nqereu  9324  1idpr  9424  map2psrpr  9504  axsup  9677  rereccl  10283  sup3  10520  infm3  10522  creur  10550  creui  10551  nndiv  10597  nnrecl  10814  rpnnen1lem1  11233  rpnnen1lem2  11234  rpnnen1lem3  11235  rpnnen1lem5  11237  supxrbnd1  11538  supxrbnd2  11539  supxrbnd  11545  rabssnn0fi  12098  mptnn0fsupp  12106  expnlbnd  12299  limsuplt  13314  clim2  13339  clim2c  13340  clim0c  13342  ello12  13351  elo12  13362  rlimresb  13400  climabs0  13420  sumeq2ii  13527  mertens  13707  prodeq2ii  13732  zprod  13756  alzdvds  14048  oddm1even  14059  divalglem4  14066  divalgb  14074  modprmn0modprm0  14344  vdwlem6  14516  vdwlem11  14521  vdw  14524  ramval  14538  imasleval  14958  dfiso3  15189  fullestrcsetc  15547  fullsetcestrc  15562  isipodrs  15918  ipodrsfi  15920  gsumpropd2lem  16027  mndpropd  16073  grppropd  16195  conjnmzb  16428  symgextfo  16574  symgfixfo  16591  sylow1lem2  16746  sylow3lem1  16774  sylow3lem3  16776  lsmelvalm  16798  lsmass  16815  iscyg3  17016  ghmcyg  17025  cycsubgcyg  17030  pgpfac1lem2  17253  pgpfac1lem4  17256  ablfac2  17267  dvdsr02  17432  crngunit  17438  dvdsrpropd  17472  lpigen  18031  znunit  18729  elfilspd  18965  scmatmats  19140  symgmatr01  19283  isclo  19715  iscnp3  19872  lmbrf  19888  cncnp  19908  lmss  19926  isnrm2  19986  cmpfi  20035  1stcfb  20072  1stccnp  20089  ptrescn  20266  txkgen  20279  xkoinjcn  20314  trfil3  20515  fmid  20587  lmflf  20632  txflf  20633  ptcmplem3  20680  tsmsf1o  20773  ucnprima  20911  metrest  21153  metcnp  21170  metcnp2  21171  txmetcnp  21176  metuel2  21208  metustblOLD  21209  metustbl  21210  metutopOLD  21211  psmetutop  21212  metucnOLD  21217  metucn  21218  evth2  21586  lmmbrf  21827  iscfil2  21831  fmcfil  21837  iscau2  21842  iscau4  21844  iscauf  21845  caucfil  21848  iscmet3lem3  21855  cfilresi  21860  causs  21863  lmclim  21867  ivth2  21993  ovolfioo  22005  ovolficc  22006  ovolshftlem1  22046  ovolscalem1  22050  volsup2  22140  ismbf3d  22187  mbfaddlem  22193  mbfsup  22197  mbfinf  22198  itg2seq  22275  itg2gt0  22293  ellimc2  22407  ellimc3  22409  rolle  22517  cmvth  22518  mvth  22519  dvlip  22520  dvivth  22537  lhop1lem  22540  deg1ldg  22618  ulm2  22906  ulmdvlem3  22923  dcubic  23303  mcubic  23304  cubic2  23305  rlimcnp  23421  ftalem3  23474  isppw2  23515  lgsquadlem2  23756  dchrmusumlema  23804  dchrisum0lema  23825  tglowdim2l  24157  mirreu3  24161  oppcom  24242  axsegcon  24357  axpasch  24371  axcontlem7  24400  clwwlkfo  24924  eclclwwlkn1  24959  el2spthonot0  24998  usg2spthonot1  25017  rusgranumwlks  25083  usgreg2spot  25194  nmobndi  25817  nmounbi  25818  nmoo0  25833  h2hcau  26023  h2hlm  26024  shsel3  26360  pjhtheu2  26461  chscllem2  26683  adjbdln  27129  branmfn  27151  pjimai  27222  chrelati  27410  cdj3lem3  27484  cdj3lem3b  27486  dfimafnf  27621  ofpreima  27661  isarchi2  27889  submarchi  27890  archirng  27892  archiabl  27902  isarchiofld  27968  ordtconlem1  28067  lmdvg  28096  esumfsup  28242  dya2icoseg2  28422  eulerpartlemgh  28514  ballotlemodife  28633  ballotlemsima  28651  erdszelem10  28841  iscvm  28901  wsuclem  29598  seglelin  29971  outsideofeu  29986  supadd  30247  ptrest  30253  mblfinlem1  30256  opnrebl  30343  opnrebl2  30344  filnetlem4  30404  lmclim2  30456  caures  30458  isbnd3b  30486  heiborlem7  30518  heiborlem10  30521  rrncmslem  30533  isdrngo2  30566  prter3  30828  elrfirn  30832  elrfirn2  30833  mrefg3  30845  diophin  30911  diophun  30912  diophren  30951  rmxycomplete  31057  wepwsolem  31191  fnwe2lem2  31201  islssfg  31220  evthiccabs  31732  clim2f  31845  clim2cf  31859  clim0cf  31863  fourierdlem73  32165  fourierdlem83  32175  dfaimafn  32453  usgra2pth0  32617  bj-finsumval0  34806  islshpsm  34848  lsatfixedN  34877  lrelat  34882  eqlkr2  34968  lshpkrlem1  34978  lfl1dim  34989  eqlkr4  35033  ishlat3N  35222  hlsupr2  35254  hlrelat5N  35268  hlrelat  35269  cvrval5  35282  cvrat42  35311  athgt  35323  3dim0  35324  islln3  35377  llnexatN  35388  islpln3  35400  islvol3  35443  islvol5  35446  isline4N  35644  polval2N  35773  4atex3  35948  cdleme0ex2N  36092  cdlemefrs29cpre1  36267  cdlemb3  36475  cdlemg33c  36577  cdlemg33e  36579  dia1dim2  36932  cdlemm10N  36988  dib1dim2  37038  diclspsn  37064  dih1dimatlem  37199  dihatexv2  37209  djhcvat42  37285  dihjat1lem  37298  dvh4dimat  37308  dvh2dimatN  37310  lcfrlem9  37420  mapdval4N  37502  mapdcv  37530  extoimad  38173