Theorem rexbidv 2873

Description: Formula-building rule for restricted existential quantifier (deduction rule). (Contributed by NM, 20-Nov-1994.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 6-Dec-2019.)

Hypothesis

Ref	Expression
rexbidv.1	|- ( ph -> ( ps <-> ch ) )

Assertion

Ref	Expression
rexbidv	|- ( 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 rexbidv

Step	Hyp	Ref	Expression
1		rexbidv.1	. . 3 |- ( ph -> ( ps <-> ch ) )
2	1	adantr 471	. 2 |- ( ( ph /\ x e. A ) -> ( ps <-> ch ) )
3	2	rexbidva 2870	1 |- ( ph -> ( E. x e. A ps <-> E. x e. A ch ) )

Syntax hints:   -> wi 4   <-> wb 189   e. wcel 1891   E.wrex 2738

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1673  ax-4 1686  ax-5 1762

This theorem depends on definitions:  df-bi 190  df-an 377  df-ex 1668  df-rex 2743

This theorem is referenced by:  2rexbidv  2878  rexralbidv  2879  rexeqbi1dv  2964  rexeqbidv  2970  cbvrex2v  2996  rspc2ev  3129  rspc3ev  3131  ceqsrex2v  3142  uniiunlem  3485  rabasiun  4252  eliun  4253  dfiin2g  4281  dfiunv2  4284  elrnmpt  5059  elrnmptg  5062  elimag  5150  fvelrnb  5895  fvelimab  5905  foelrn  6025  foco2  6026  elabrex  6134  abrexco  6135  f1oiso  6228  f1oiso2  6229  grprinvlem  6495  orduninsuc  6658  funcnvuni  6734  fun11iun  6741  abrexex2g  6758  abrexex2  6762  f1oweALT  6765  el2xptp  6824  tfrlem12  7094  seqomlem2  7155  nneob  7340  qseq2  7401  elqsg  7402  elixpsn  7548  ixpsnf1o  7549  isfi  7580  enfi  7775  pssnn  7777  frfi  7803  unblem1  7810  unblem2  7811  unbnn2  7815  fofinf1o  7839  finsschain  7868  indexfi  7869  elfi  7914  marypha1lem  7934  supeq3  7950  supmo  7953  suplub  7961  supisolem  7976  eqinf  7987  infval  7989  infglb  7993  infglbb  7994  infmo  7998  oieq1  8014  ordtypelem2  8021  ordtypelem3  8022  ordtypelem9  8028  wemaplem1  8048  brwdom2  8075  brwdom3  8084  unwdomg  8086  oemapval  8175  cantnf  8185  wemapwe  8189  cnfcom3clem  8197  tz9.13  8249  tz9.13g  8250  cardf2  8364  isnum2  8366  ennum  8368  cardiun  8403  infxpenc2  8440  aceq1  8535  aceq2  8537  dfac5lem3  8543  dfac5lem4  8544  dfac2a  8547  dfac2  8548  kmlem9  8575  kmlem12  8578  kmlem14  8580  ackbij1  8655  cflm  8667  cfss  8682  cofsmo  8686  cfsmolem  8687  cfcoflem  8689  coftr  8690  isfin7  8718  fin23lem26  8742  isf32lem5  8774  fin1a2lem11  8827  hsmexlem2  8844  axdc3lem3  8869  axdc3  8871  numthcor  8911  zorn2lem7  8919  brdom3  8943  brdom7disj  8946  brdom6disj  8947  iundom2g  8952  fpwwe2  9055  winainflem  9105  winalim2  9108  inar1  9187  tskuni  9195  nqereu  9341  prnmax  9407  genpv  9411  genpnmax  9419  genpass  9421  prlem936  9459  recexsrlem  9514  map2psrpr  9521  supsrlem  9522  axrrecex  9574  axpre-sup  9580  dedekind  9784  cnegex  9801  recex  10233  fimaxre3  10542  infm3  10557  supaddc  10563  supadd  10564  supmul1  10565  supmullem1  10566  supmullem2  10567  supmul  10568  creur  10592  creui  10593  cju  10594  nnunb  10855  arch  10856  xrsupsslem  11582  xrinfmsslem  11583  xrsupss  11584  xrinfmss  11585  xrub  11587  supxrunb1  11595  supxrunb2  11596  infmxrgelbOLD  11615  infmremnf  11623  infmrp1  11624  fsequb2  12183  hashge2el2difr  12633  iswrd  12667  iswrdOLD  12668  wrdval  12669  csbwrdg  12694  cshword  12892  0csh0  12894  2cshwcshw  12923  scshwfzeqfzo  12924  shftfval  13144  abs1m  13409  rexfiuz  13421  limsupbnd2  13557  limsupbnd2OLD  13558  clim  13569  rlim  13570  rlim2  13571  rlim0  13583  rlim0lt  13584  ello1mpt2  13597  o1lo1  13612  o1compt  13662  rlimdiv  13720  climsup  13744  sumeq1  13766  sumeq2w  13769  summo  13794  fsum  13797  fsumcvg3  13806  infcvgaux2i  13927  mertenslem1  13951  mertenslem2  13952  mertens  13953  prodeq1f  13973  prodeq2w  13977  prodmo  14001  fprod  14006  divides  14318  odd2np1lem  14375  divalglem4  14386  divalglem10  14394  divalg  14395  gcdcllem3  14486  bezoutlem1  14514  exprmfct  14659  nnnn0modprm0  14768  opeo  14774  omeo  14775  pythagtriplem2  14778  pythagtrip  14795  pceu  14807  pcprmpw2  14842  unbenlem  14863  4sqlem12  14911  vdwapval  14934  vdwapun  14935  vdwmc2  14940  vdwpc  14941  vdwlem2  14943  vdwlem10  14951  vdwlem13  14954  vdwnnlem1  14956  rami  14983  cshwsiun  15081  cshwrepswhash1  15084  brssc  15730  isdrs  16190  drsdir  16191  drsdirfi  16194  isdrs2  16195  ipodrsima  16422  gsumvalx  16524  gsumpropd  16526  gsumress  16530  isnsgrp  16542  sgrp2nmndlem5  16674  grpinvex  16692  grp1  16769  imasgrp2  16812  conjnmzb  16928  gaorb  16972  orbsta  16978  symgfix2  17068  symgextfo  17074  pmtrprfvalrn  17140  psgnunilem3  17148  psgneu  17158  psgnval  17159  psgnvali  17160  psgnvalii  17161  ispgp  17255  subgpgp  17260  sylow1  17266  pgpfi  17268  sylow2blem3  17285  fislw  17288  sylow3lem2  17291  lsmelvalm  17314  lsmass  17331  pj1fval  17355  pj1val  17356  pj1eu  17357  pj1id  17360  efgrelexlema  17410  efgrelexlemb  17411  efgredeu  17413  cyggeninv  17529  cygabl  17536  pgpfac1lem2  17719  pgpfac1lem3  17721  pgpfac1lem4  17722  pgpfac1  17724  pgpfaclem2  17726  pgpfac  17728  dvdsrval  17884  dvdsr  17885  subrgdvds  18033  lss1d  18197  lspsn  18236  lspsnel  18237  lspsolvlem  18376  rspsn  18489  opsrval  18709  znf1o  19133  cygznlem3  19151  psgndiflemA  19180  ellspd  19371  mat1dimelbas  19507  mat1dimbas  19508  scmatval  19540  scmatel  19541  scmateALT  19548  mat0scmat  19574  decpmataa0  19803  decpmatmulsumfsupp  19808  pmatcollpw2lem  19812  pm2mpmhmlem1  19853  chpscmat  19877  basis2  19977  eltg2  19984  tg2  19991  isclo  20114  neival  20129  isnei  20130  isneip  20132  restbas  20185  neitr  20207  cnpval  20263  iscnp  20264  cnpimaex  20283  lmbr  20285  lmbr2  20286  cnprest2  20317  lmff  20328  regsep  20361  pnrmopn  20370  nrmsep3  20382  isnrm2  20385  iscmp  20414  cmpsublem  20425  cmpsub  20426  tgcmp  20427  sscmp  20431  hauscmplem  20432  1stcclb  20470  1stcfb  20471  is2ndc  20472  2ndc1stc  20477  1stcrest  20479  2ndcctbss  20481  1stcelcls  20487  llyeq  20496  nllyeq  20497  hausllycmp  20520  lly1stc  20522  refssex  20537  refun0  20541  islocfin  20543  locfinnei  20549  comppfsc  20558  txbas  20593  ptval  20596  ptpjopn  20638  ptclsg  20641  txcnp  20646  ptcnp  20648  txrest  20657  ptrescn  20665  txcmp  20669  tx1stc  20676  xkococn  20686  kqreglem1  20767  fbasssin  20862  fbssfi  20863  fbssint  20864  fbun  20866  fgss2  20900  fgcl  20904  ufli  20940  fmfnfmlem3  20982  fbflim2  21003  hauspwpwf1  21013  flfneii  21018  flftg  21022  txflf  21032  fclscf  21051  alexsubb  21072  alexsubALT  21077  tsmssubm  21168  ustincl  21233  ustdiag  21234  ustinvel  21235  ustexhalf  21236  ust0  21245  trust  21255  elutop  21259  ucnval  21303  ucncn  21311  cfiluexsm  21316  cfiluweak  21321  blssps  21450  blss  21451  imasf1oxms  21515  mopni  21518  metss  21534  metrest  21550  metcnp3  21566  cfilucfil  21585  metuel2  21591  nlmvscn  21701  nrginvrcn  21705  icccmplem1  21851  icccmplem2  21852  icccmp  21854  divcn  21911  cncfval  21931  elcncf2  21933  cncfmet  21951  cnheibor  21994  evth  21998  lebnumlem3  22002  lebnumlem3OLD  22005  lebnum  22006  xlebnum  22007  lebnumii  22008  ipcn  22228  lmmbr  22239  lmmbr2  22240  cfilfval  22245  cfili  22249  iscfil3  22254  caufval  22256  iscau  22257  iscau2  22258  equivcfil  22280  equivcau  22281  lmcau  22293  ovolval  22437  ovolvalOLD  22438  elovolm  22439  ovolgelb  22444  ovoliunlem1  22466  ovoliun2  22470  ovolshftlem1  22473  ovolscalem1  22477  ovolicc  22488  ioombl1lem4  22526  uniioombllem2  22552  uniioombllem2OLD  22553  mbfaddlem  22628  mbfsup  22632  mbfinf  22633  mbfinfOLD  22634  mbflimsup  22635  mbflimsupOLD  22636  i1fmulc  22673  itg1climres  22684  itg2val  22698  itg2l  22699  itg2leub  22704  itg2seq  22712  itg2monolem1  22720  itg2mono  22723  itg2i1fseq2  22726  cniccibl  22810  ellimc3  22846  limciun  22861  dvferm1  22949  dvferm2  22951  lhop1lem  22977  ply1divex  23099  ig1peu  23134  ig1peuOLD  23135  plyval  23159  elply2  23162  coeval  23189  coeeu  23191  coelem  23192  coeeq  23193  plydivlem4  23261  plydivex  23262  aannenlem2  23297  aalioulem2  23301  aaliou2  23308  ulmval  23347  ulm2  23352  ulmcau  23362  ulmdvlem3  23369  abelthlem9  23407  abelth  23408  efif1olem4  23506  eflogeq  23563  efopn  23615  cxpcn3  23700  cxpeq  23709  rlimcnp  23903  lgamgulmlem6  23971  muval  24071  dchrptlem1  24204  dchrptlem2  24205  lgsdchrval  24287  pntpbnd  24438  pntibndlem3  24442  pntibnd  24443  pntlemi  24454  pntleme  24458  pntlemp  24460  pnt3  24462  istrkgld  24519  istrkg3ld  24521  axtgsegcon  24524  axtgpasch  24527  axtgcont1  24528  axtgupdim2  24531  legov  24642  islnopp  24793  ishpg  24813  hpgbr  24814  hpgcom  24821  iscgra  24863  iscgra1  24864  isinag  24891  isleag  24895  ttgval  24917  ttgitvval  24924  ttgelitv  24925  brbtwn  24941  brcgr  24942  axpasch  24983  axlowdim2  25002  axlowdim  25003  axcontlem2  25007  axcontlem4  25009  axcontlem7  25012  axcontlem8  25013  nbgraf1olem1  25181  cusgrafilem2  25220  cusgrafi  25222  wwlkn0  25429  clwwlknscsh  25559  erclwwlkneq  25563  eclclwwlkn0  25571  eleclclwwlkn  25573  hashecclwwlkn1  25574  usghashecclwwlk  25575  el2wlksot  25620  el2pthsot  25621  2spot2iun2spont  25631  iseupa  25705  3cyclfrgrarn1  25752  usgn0fidegnn0  25769  frgrancvvdeqlem4  25773  friendshipgt3  25861  isgrpo  25936  isgrpoi  25938  grpoidinvlem3  25946  grpoideu  25949  grpoidinv2  25958  isgrp2d  25975  isgrpda  26037  ghgrpOLD  26108  rngoid  26123  nmoofval  26415  nmooval  26416  nmosetn0  26418  nmoolb  26424  nmoubi  26425  nmlno0lem  26446  chcompl  26907  pjhthmo  26967  pjhval  27062  pjpreeq  27063  h1de2ci  27221  elspansn  27231  nmopval  27521  nmopsetn0  27530  nmfnval  27541  nmfnsetn0  27543  eigvecval  27561  hhcno  27569  hhcnf  27570  nmoplb  27572  nmopub  27573  nmfnlb  27589  nmfnleub  27590  eleigvec  27622  nmlnop0iALT  27660  nmopun  27679  nmcexi  27691  branmfn  27770  pjnmopi  27813  cvbr  27947  hatomic  28025  chrelat2  28035  cdjreui  28097  cdj3lem2  28100  reuxfr4d  28138  elabreximd  28156  br8d  28227  unipreima  28254  abfmpunirn  28260  curry2ima  28297  infxrge0glbOLD  28357  toslublem  28436  tosglblem  28438  archirng  28512  archiexdiv  28514  archiabllem2a  28518  archiabl  28522  isarchiofld  28587  crefi  28681  pcmplfin  28694  pstmfval  28706  tpr2rico  28725  rge0scvg  28762  ismntop  28837  esumc  28879  esumpcvgval  28906  esum2dlem  28920  inelsros  29007  diffiunisros  29008  dya2icoseg2  29106  dya2iocuni  29111  eulerpartlemgvv  29215  eulerpartlemgh  29217  bnj66  29677  bnj873  29741  bnj18eq1  29744  bnj1234  29828  bnj1318  29840  subfacp1lem3  29911  pconcn  29953  cnpcon  29959  txpcon  29961  conpcon  29964  iscvm  29988  cvmcov  29992  cvmopnlem  30007  cvmliftlem15  30027  cvmlift3lem2  30049  cvmlift3lem4  30051  cvmlift3  30057  br8  30402  br6  30403  br4  30404  dfrdg2  30448  dfrdg3  30449  orderseqlem  30496  poseq  30497  soseq  30498  elno  30539  sltval  30540  nobndlem6  30592  nofulllem1  30597  nofulllem2  30598  nofulllem5  30601  altxpeq2  30747  funtransport  30804  fvtransport  30805  brcolinear2  30831  colineardim1  30834  segcon2  30878  brsegle  30881  funray  30913  fvray  30914  funline  30915  linedegen  30916  fvline  30917  ellines  30925  gtinf  30981  nn0prpwlem  30984  fnessref  31019  neibastop2lem  31022  neibastop2  31023  tailfb  31039  bj-finsumval0  31704  relowlssretop  31768  phpreu  31931  ptrest  31941  poimirlem4  31946  poimirlem17  31959  poimirlem20  31962  poimirlem24  31966  poimirlem26  31968  poimirlem27  31969  poimirlem28  31970  poimirlem31  31973  poimirlem32  31974  poimir  31975  heicant  31977  mblfinlem1  31979  mblfinlem3  31981  mblfinlem4  31982  ismblfin  31983  itg2addnclem  31995  itg2addnclem3  31997  itg2addnc  31998  itg2gt0cn  31999  cnicciblnc  32015  ftc1anclem6  32024  unirep  32041  indexa  32062  sdclem2  32073  sdclem1  32074  sdc  32075  fdc  32076  fdc1  32077  incsequz  32079  istotbnd  32103  sstotbnd2  32108  equivtotbnd  32112  isbnd  32114  bndss  32120  ssbnd  32122  totbndbnd  32123  ismtybndlem  32140  heibor1lem  32143  heiborlem1  32145  heiborlem6  32150  heiborlem8  32152  heiborlem10  32154  heibor  32155  isdrngo2  32199  divrngidl  32263  prnc  32302  isfldidl  32303  prtlem5  32432  prtlem13  32442  prtlem16  32443  islshp  32547  lsmsat  32576  lcvbr  32589  lsatcv0  32599  lshpsmreu  32677  lshpkrlem1  32678  lshpkrlem2  32679  lshpkrlem3  32680  lshpkrcl  32684  lshpset2N  32687  islshpkrN  32688  cvrval  32837  atlex  32884  glbconxN  32945  hlsuprexch  32948  islln  33073  islpln  33097  islpln5  33102  lvolex3N  33105  islvol  33140  islvol5  33146  ispointN  33309  pmapglbx  33336  paddval  33365  elpaddn0  33367  elpaddat  33371  elpadd0  33376  4atex  33643  4atex2  33644  cdlemefrs29bpre1  33966  cdlemefrs32fva  33969  cdlemg33b  34276  dvhb1dimN  34555  dvhopellsm  34687  dib1dim  34735  diclspsn  34764  dihglblem2aN  34863  dihglblem2N  34864  dih1dimatlem  34899  dvh3dimatN  35009  dvh2dim  35015  dvh3dim  35016  dvh4dimN  35017  dvh3dim3N  35019  dochfl1  35046  lcfl7N  35071  lcf1o  35121  lcfrlem39  35151  mapdpglem3  35245  hvmapvalvalN  35331  hdmap14lem2a  35440  hdmapglem7a  35500  elrfi  35538  isnacs  35548  nacsfg  35549  nacsfix  35556  mzpcompact2lem  35595  eldiophb  35601  eldioph  35602  eldioph2  35606  eldioph2b  35607  eldioph3  35610  eldiophss  35619  diophrex  35620  sbcrexgOLD  35630  sbc2rexgOLD  35633  rexrabdioph  35639  rexfrabdioph  35640  elnn0rabdioph  35648  dvdsrabdioph  35655  eldioph4b  35656  eldioph4i  35657  diophren  35658  rencldnfilem  35665  pell1234qrdich  35709  jm2.27  35865  expdiophlem1  35878  wepwsolem  35902  aomclem8  35921  islnr3  35976  lnr2i  35977  lpirlnr  35978  hbtlem1  35984  hbtlem2  35985  hbtlem7  35986  hbtlem4  35987  hbtlem5  35989  hbtlem6  35990  dgraaval  36007  dgraavalOLD  36008  dgraalem  36009  dgraalemOLD  36010  dgraaub  36015  dgraaubOLD  36016  rngunsnply  36041  brtrclfv2  36321  extoimad  36609  elabrexg  37366  foelrnf  37471  disjrnmpt2  37473  upbdrech  37554  ssfiunibd  37558  supxrgere  37587  supxrgelem  37591  supxrge  37592  suplesup  37593  infxr  37622  infleinf  37627  iccshift  37660  iooshift  37664  infrglbOLD  37711  climinf  37726  climinfOLD  37727  climinff  37732  climinffOLD  37733  ellimcabssub0  37739  climf  37744  limcperiod  37750  limclner  37774  cncfshiftioo  37812  fperdvper  37832  itgiccshift  37899  itgperiod  37900  stoweidlem27  37944  stoweidlem31  37949  stoweidlem43  37961  stoweidlem46  37964  stoweidlem52  37970  stoweidlem60  37978  fourierdlem42  38069  fourierdlem42OLD  38070  fourierdlem48  38075  fourierdlem51  38078  fourierdlem54  38081  fourierdlem63  38090  fourierdlem64  38091  fourierdlem65  38092  fourierdlem68  38095  fourierdlem70  38097  fourierdlem71  38098  fourierdlem73  38100  fourierdlem80  38107  fourierdlem81  38108  fourierdlem89  38116  fourierdlem90  38117  fourierdlem91  38118  fourierdlem92  38119  fourierdlem96  38123  fourierdlem97  38124  fourierdlem98  38125  fourierdlem99  38126  fourierdlem100  38127  fourierdlem103  38130  fourierdlem104  38131  fourierdlem105  38132  fourierdlem108  38135  fourierdlem109  38136  fourierdlem110  38137  fourierdlem112  38139  fourierdlem113  38140  sge0pnffigt  38297  sge0resplit  38307  ovnval2  38430  ovnval2b  38437  ovnlecvr  38443  ovnpnfelsup  38444  ovn0lem  38450  ovnsubaddlem1  38455  hoidmvlelem1  38480  ovnhoilem1  38486  ovnhoi  38488  ovnlecvr2  38495  hoiqssbl  38510  ovolval5lem2  38538  ovolval5lem3  38539  ovolval5  38540  ovnovol  38544  cbvrex2  38685  afvelrnb  38756  afvelrnb0  38757  iccelpart  38838  iccpartiun  38839  icceuelpart  38841  m1expevenALTV  38868  odd2np1ALTV  38894  opoeALTV  38903  opeoALTV  38904  isgbo  38944  isgboa  38945  7gbo  38964  9gboa  38966  11gboa  38967  bgoldbwt  38969  nnsum3primesgbe  38978  nnsum4primesodd  38982  nnsum4primesoddALTV  38983  bgoldbtbnd  38995  cshword2  39071  n0snor2el  39089  upgredg2vtx  39331  usgredg4  39396  ushgredgedga  39408  ushgredgedgaloop  39410  dfnbgr2  39509  nbgrel  39512  nbumgrvtx  39516  nbgrnself  39531  uvtxael1  39570  uvtxa01vtx0  39571  cusgrfilem2  39619  cusgrfi  39621  uhgrvd0nedgb  39647  0nodd  40135  1odd  40136  2nodd  40137  0even  40256  1neven  40257  2even  40258  2zlidl  40259  2zrngamgm  40264  2zrngagrp  40268  2zrngmmgm  40271  2zrngnmrid  40275  lcoval  40530  el0ldep  40584  ldepspr  40591  zlmodzxzldep  40622