Theorem rexbidv 2936

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 466	. 2 |- ( ( ph /\ x e. A ) -> ( ps <-> ch ) )
3	2	rexbidva 2933	1 |- ( ph -> ( E. x e. A ps <-> E. x e. A ch ) )

Syntax hints:   -> wi 4   <-> wb 187   e. wcel 1872   E.wrex 2772

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752

This theorem depends on definitions:  df-bi 188  df-an 372  df-ex 1658  df-rex 2777

This theorem is referenced by:  rexbiiOLD  2938  2rexbidv  2943  rexralbidv  2944  rexeqbi1dv  3031  rexeqbidv  3037  cbvrex2v  3063  rspc2ev  3193  rspc3ev  3195  ceqsrex2v  3206  uniiunlem  3549  rabasiun  4303  eliun  4304  dfiin2g  4332  dfiunv2  4335  elrnmpt  5100  elrnmptg  5103  elimag  5191  fvelrnb  5928  fvelimab  5937  foelrn  6056  foco2  6057  elabrex  6163  abrexco  6164  f1oiso  6257  f1oiso2  6258  grprinvlem  6521  orduninsuc  6684  funcnvuni  6760  fun11iun  6767  abrexex2g  6784  abrexex2  6788  f1oweALT  6791  el2xptp  6850  tfrlem12  7118  seqomlem2  7179  nneob  7364  qseq2  7425  elqsg  7426  elixpsn  7572  ixpsnf1o  7573  isfi  7603  enfi  7797  pssnn  7799  frfi  7825  unblem1  7832  unblem2  7833  unbnn2  7837  fofinf1o  7861  finsschain  7890  indexfi  7891  elfi  7936  marypha1lem  7956  supeq3  7972  supmo  7975  suplub  7983  supisolem  7998  eqinf  8009  infval  8011  infglb  8015  infglbb  8016  infmo  8020  oieq1  8036  ordtypelem2  8043  ordtypelem3  8044  ordtypelem9  8050  wemaplem1  8070  brwdom2  8097  brwdom3  8106  unwdomg  8108  oemapval  8196  cantnf  8206  wemapwe  8210  cnfcom3clem  8218  tz9.13  8270  tz9.13g  8271  cardf2  8385  isnum2  8387  ennum  8389  cardiun  8424  infxpenc2  8460  aceq1  8555  aceq2  8557  dfac5lem3  8563  dfac5lem4  8564  dfac2a  8567  dfac2  8568  kmlem9  8595  kmlem12  8598  kmlem14  8600  ackbij1  8675  cflm  8687  cfss  8702  cofsmo  8706  cfsmolem  8707  cfcoflem  8709  coftr  8710  isfin7  8738  fin23lem26  8762  isf32lem5  8794  fin1a2lem11  8847  hsmexlem2  8864  axdc3lem3  8889  axdc3  8891  numthcor  8931  zorn2lem7  8939  brdom3  8963  brdom7disj  8966  brdom6disj  8967  iundom2g  8972  fpwwe2  9075  winainflem  9125  winalim2  9128  inar1  9207  tskuni  9215  nqereu  9361  prnmax  9427  genpv  9431  genpnmax  9439  genpass  9441  prlem936  9479  recexsrlem  9534  map2psrpr  9541  supsrlem  9542  axrrecex  9594  axpre-sup  9600  dedekind  9804  cnegex  9821  recex  10251  fimaxre3  10560  infm3  10575  supaddc  10581  supadd  10582  supmul1  10583  supmullem1  10584  supmullem2  10585  supmul  10586  creur  10610  creui  10611  cju  10612  nnunb  10872  arch  10873  xrsupsslem  11599  xrinfmsslem  11600  xrsupss  11601  xrinfmss  11602  xrub  11604  supxrunb1  11612  supxrunb2  11613  infmxrgelbOLD  11632  infmremnf  11640  infmrp1  11641  fsequb2  12195  hashge2el2difr  12642  iswrd  12676  iswrdOLD  12677  wrdval  12678  csbwrdg  12700  cshword  12895  0csh0  12897  2cshwcshw  12926  scshwfzeqfzo  12927  shftfval  13133  abs1m  13398  rexfiuz  13410  limsupbnd2  13545  limsupbnd2OLD  13546  clim  13557  rlim  13558  rlim2  13559  rlim0  13571  rlim0lt  13572  ello1mpt2  13585  o1lo1  13600  o1compt  13650  rlimdiv  13708  climsup  13732  sumeq1  13754  sumeq2w  13757  summo  13782  fsum  13785  fsumcvg3  13794  infcvgaux2i  13915  mertenslem1  13939  mertenslem2  13940  mertens  13941  prodeq1f  13961  prodeq2w  13965  prodmo  13989  fprod  13994  divides  14306  odd2np1lem  14363  divalglem4  14374  divalglem10  14382  divalg  14383  gcdcllem3  14474  bezoutlem1  14502  exprmfct  14647  nnnn0modprm0  14756  opeo  14762  omeo  14763  pythagtriplem2  14766  pythagtrip  14783  pceu  14795  pcprmpw2  14830  unbenlem  14851  4sqlem12  14899  vdwapval  14922  vdwapun  14923  vdwmc2  14928  vdwpc  14929  vdwlem2  14931  vdwlem10  14939  vdwlem13  14942  vdwnnlem1  14944  rami  14971  cshwsiun  15069  cshwrepswhash1  15072  brssc  15718  isdrs  16178  drsdir  16179  drsdirfi  16182  isdrs2  16183  ipodrsima  16410  gsumvalx  16512  gsumpropd  16514  gsumress  16518  isnsgrp  16530  sgrp2nmndlem5  16662  grpinvex  16680  grp1  16757  imasgrp2  16800  conjnmzb  16916  gaorb  16960  orbsta  16966  symgfix2  17056  symgextfo  17062  pmtrprfvalrn  17128  psgnunilem3  17136  psgneu  17146  psgnval  17147  psgnvali  17148  psgnvalii  17149  ispgp  17243  subgpgp  17248  sylow1  17254  pgpfi  17256  sylow2blem3  17273  fislw  17276  sylow3lem2  17279  lsmelvalm  17302  lsmass  17319  pj1fval  17343  pj1val  17344  pj1eu  17345  pj1id  17348  efgrelexlema  17398  efgrelexlemb  17399  efgredeu  17401  cyggeninv  17517  cygabl  17524  pgpfac1lem2  17707  pgpfac1lem3  17709  pgpfac1lem4  17710  pgpfac1  17712  pgpfaclem2  17714  pgpfac  17716  dvdsrval  17872  dvdsr  17873  subrgdvds  18021  lss1d  18185  lspsn  18224  lspsnel  18225  lspsolvlem  18364  rspsn  18477  opsrval  18697  znf1o  19120  cygznlem3  19138  psgndiflemA  19167  ellspd  19358  mat1dimelbas  19494  mat1dimbas  19495  scmatval  19527  scmatel  19528  scmateALT  19535  mat0scmat  19561  decpmataa0  19790  decpmatmulsumfsupp  19795  pmatcollpw2lem  19799  pm2mpmhmlem1  19840  chpscmat  19864  basis2  19964  eltg2  19971  tg2  19978  isclo  20101  neival  20116  isnei  20117  isneip  20119  restbas  20172  neitr  20194  cnpval  20250  iscnp  20251  cnpimaex  20270  lmbr  20272  lmbr2  20273  cnprest2  20304  lmff  20315  regsep  20348  pnrmopn  20357  nrmsep3  20369  isnrm2  20372  iscmp  20401  cmpsublem  20412  cmpsub  20413  tgcmp  20414  sscmp  20418  hauscmplem  20419  1stcclb  20457  1stcfb  20458  is2ndc  20459  2ndc1stc  20464  1stcrest  20466  2ndcctbss  20468  1stcelcls  20474  llyeq  20483  nllyeq  20484  hausllycmp  20507  lly1stc  20509  refssex  20524  refun0  20528  islocfin  20530  locfinnei  20536  comppfsc  20545  txbas  20580  ptval  20583  ptpjopn  20625  ptclsg  20628  txcnp  20633  ptcnp  20635  txrest  20644  ptrescn  20652  txcmp  20656  tx1stc  20663  xkococn  20673  kqreglem1  20754  fbasssin  20849  fbssfi  20850  fbssint  20851  fbun  20853  fgss2  20887  fgcl  20891  ufli  20927  fmfnfmlem3  20969  fbflim2  20990  hauspwpwf1  21000  flfneii  21005  flftg  21009  txflf  21019  fclscf  21038  alexsubb  21059  alexsubALT  21064  tsmssubm  21155  ustincl  21220  ustdiag  21221  ustinvel  21222  ustexhalf  21223  ust0  21232  trust  21242  elutop  21246  ucnval  21290  ucncn  21298  cfiluexsm  21303  cfiluweak  21308  blssps  21437  blss  21438  imasf1oxms  21502  mopni  21505  metss  21521  metrest  21537  metcnp3  21553  cfilucfil  21572  metuel2  21578  nlmvscn  21688  nrginvrcn  21692  icccmplem1  21838  icccmplem2  21839  icccmp  21841  divcn  21898  cncfval  21918  elcncf2  21920  cncfmet  21938  cnheibor  21981  evth  21985  lebnumlem3  21989  lebnumlem3OLD  21992  lebnum  21993  xlebnum  21994  lebnumii  21995  ipcn  22215  lmmbr  22226  lmmbr2  22227  cfilfval  22232  cfili  22236  iscfil3  22241  caufval  22243  iscau  22244  iscau2  22245  equivcfil  22267  equivcau  22268  lmcau  22280  ovolval  22424  ovolvalOLD  22425  elovolm  22426  ovolgelb  22431  ovoliunlem1  22453  ovoliun2  22457  ovolshftlem1  22460  ovolscalem1  22464  ovolicc  22475  ioombl1lem4  22512  uniioombllem2  22538  uniioombllem2OLD  22539  mbfaddlem  22614  mbfsup  22618  mbfinf  22619  mbfinfOLD  22620  mbflimsup  22621  mbflimsupOLD  22622  i1fmulc  22659  itg1climres  22670  itg2val  22684  itg2l  22685  itg2leub  22690  itg2seq  22698  itg2monolem1  22706  itg2mono  22709  itg2i1fseq2  22712  cniccibl  22796  ellimc3  22832  limciun  22847  dvferm1  22935  dvferm2  22937  lhop1lem  22963  ply1divex  23085  ig1peu  23120  ig1peuOLD  23121  plyval  23145  elply2  23148  coeval  23175  coeeu  23177  coelem  23178  coeeq  23179  plydivlem4  23247  plydivex  23248  aannenlem2  23283  aalioulem2  23287  aaliou2  23294  ulmval  23333  ulm2  23338  ulmcau  23348  ulmdvlem3  23355  abelthlem9  23393  abelth  23394  efif1olem4  23492  eflogeq  23549  efopn  23601  cxpcn3  23686  cxpeq  23695  rlimcnp  23889  lgamgulmlem6  23957  muval  24057  dchrptlem1  24190  dchrptlem2  24191  lgsdchrval  24273  pntpbnd  24424  pntibndlem3  24428  pntibnd  24429  pntlemi  24440  pntleme  24444  pntlemp  24446  pnt3  24448  istrkgld  24505  istrkg3ld  24507  axtgsegcon  24510  axtgpasch  24513  axtgcont1  24514  axtgupdim2  24517  legov  24628  islnopp  24779  ishpg  24799  hpgbr  24800  hpgcom  24807  iscgra  24849  iscgra1  24850  isinag  24877  isleag  24881  ttgval  24903  ttgitvval  24910  ttgelitv  24911  brbtwn  24927  brcgr  24928  axpasch  24969  axlowdim2  24988  axlowdim  24989  axcontlem2  24993  axcontlem4  24995  axcontlem7  24998  axcontlem8  24999  nbgraf1olem1  25167  cusgrafilem2  25206  cusgrafi  25208  wwlkn0  25415  clwwlknscsh  25545  erclwwlkneq  25549  eclclwwlkn0  25557  eleclclwwlkn  25559  hashecclwwlkn1  25560  usghashecclwwlk  25561  el2wlksot  25606  el2pthsot  25607  2spot2iun2spont  25617  iseupa  25691  3cyclfrgrarn1  25738  usgn0fidegnn0  25755  frgrancvvdeqlem4  25759  friendshipgt3  25847  isgrpo  25922  isgrpoi  25924  grpoidinvlem3  25932  grpoideu  25935  grpoidinv2  25944  isgrp2d  25961  isgrpda  26023  ghgrpOLD  26094  rngoid  26109  nmoofval  26401  nmooval  26402  nmosetn0  26404  nmoolb  26410  nmoubi  26411  nmlno0lem  26432  chcompl  26893  pjhthmo  26953  pjhval  27048  pjpreeq  27049  h1de2ci  27207  elspansn  27217  nmopval  27507  nmopsetn0  27516  nmfnval  27527  nmfnsetn0  27529  eigvecval  27547  hhcno  27555  hhcnf  27556  nmoplb  27558  nmopub  27559  nmfnlb  27575  nmfnleub  27576  eleigvec  27608  nmlnop0iALT  27646  nmopun  27665  nmcexi  27677  branmfn  27756  pjnmopi  27799  cvbr  27933  hatomic  28011  chrelat2  28021  cdjreui  28083  cdj3lem2  28086  reuxfr4d  28124  elabreximd  28143  br8d  28220  unipreima  28247  abfmpunirn  28253  curry2ima  28291  infxrge0glbOLD  28355  toslublem  28435  tosglblem  28437  archirng  28512  archiexdiv  28514  archiabllem2a  28518  archiabl  28522  isarchiofld  28588  crefi  28682  pcmplfin  28695  pstmfval  28707  tpr2rico  28726  rge0scvg  28763  ismntop  28838  esumc  28880  esumpcvgval  28907  esum2dlem  28921  inelsros  29008  diffiunisros  29009  dya2icoseg2  29108  dya2iocuni  29113  eulerpartlemgvv  29217  eulerpartlemgh  29219  bnj66  29679  bnj873  29743  bnj18eq1  29746  bnj1234  29830  bnj1318  29842  subfacp1lem3  29913  pconcn  29955  cnpcon  29961  txpcon  29963  conpcon  29966  iscvm  29990  cvmcov  29994  cvmopnlem  30009  cvmliftlem15  30029  cvmlift3lem2  30051  cvmlift3lem4  30053  cvmlift3  30059  br8  30403  br6  30404  br4  30405  dfrdg2  30449  dfrdg3  30450  orderseqlem  30497  poseq  30498  soseq  30499  elno  30540  sltval  30541  nobndlem6  30591  nofulllem1  30596  nofulllem2  30597  nofulllem5  30600  altxpeq2  30746  funtransport  30803  fvtransport  30804  brcolinear2  30830  colineardim1  30833  segcon2  30877  brsegle  30880  funray  30912  fvray  30913  funline  30914  linedegen  30915  fvline  30916  ellines  30924  gtinf  30980  nn0prpwlem  30983  fnessref  31018  neibastop2lem  31021  neibastop2  31022  tailfb  31038  bj-finsumval0  31666  relowlssretop  31730  phpreu  31893  ptrest  31903  poimirlem4  31908  poimirlem17  31921  poimirlem20  31924  poimirlem24  31928  poimirlem26  31930  poimirlem27  31931  poimirlem28  31932  poimirlem31  31935  poimirlem32  31936  poimir  31937  heicant  31939  mblfinlem1  31941  mblfinlem3  31943  mblfinlem4  31944  ismblfin  31945  itg2addnclem  31957  itg2addnclem3  31959  itg2addnc  31960  itg2gt0cn  31961  cnicciblnc  31977  ftc1anclem6  31986  unirep  32003  indexa  32024  sdclem2  32035  sdclem1  32036  sdc  32037  fdc  32038  fdc1  32039  incsequz  32041  istotbnd  32065  sstotbnd2  32070  equivtotbnd  32074  isbnd  32076  bndss  32082  ssbnd  32084  totbndbnd  32085  ismtybndlem  32102  heibor1lem  32105  heiborlem1  32107  heiborlem6  32112  heiborlem8  32114  heiborlem10  32116  heibor  32117  isdrngo2  32161  divrngidl  32225  prnc  32264  isfldidl  32265  prtlem5  32396  prtlem13  32408  prtlem16  32409  islshp  32514  lsmsat  32543  lcvbr  32556  lsatcv0  32566  lshpsmreu  32644  lshpkrlem1  32645  lshpkrlem2  32646  lshpkrlem3  32647  lshpkrcl  32651  lshpset2N  32654  islshpkrN  32655  cvrval  32804  atlex  32851  glbconxN  32912  hlsuprexch  32915  islln  33040  islpln  33064  islpln5  33069  lvolex3N  33072  islvol  33107  islvol5  33113  ispointN  33276  pmapglbx  33303  paddval  33332  elpaddn0  33334  elpaddat  33338  elpadd0  33343  4atex  33610  4atex2  33611  cdlemefrs29bpre1  33933  cdlemefrs32fva  33936  cdlemg33b  34243  dvhb1dimN  34522  dvhopellsm  34654  dib1dim  34702  diclspsn  34731  dihglblem2aN  34830  dihglblem2N  34831  dih1dimatlem  34866  dvh3dimatN  34976  dvh2dim  34982  dvh3dim  34983  dvh4dimN  34984  dvh3dim3N  34986  dochfl1  35013  lcfl7N  35038  lcf1o  35088  lcfrlem39  35118  mapdpglem3  35212  hvmapvalvalN  35298  hdmap14lem2a  35407  hdmapglem7a  35467  elrfi  35505  isnacs  35515  nacsfg  35516  nacsfix  35523  mzpcompact2lem  35562  eldiophb  35568  eldioph  35569  eldioph2  35573  eldioph2b  35574  eldioph3  35577  eldiophss  35586  diophrex  35587  sbcrexgOLD  35597  sbc2rexgOLD  35600  rexrabdioph  35606  rexfrabdioph  35607  elnn0rabdioph  35615  dvdsrabdioph  35622  eldioph4b  35623  eldioph4i  35624  diophren  35625  rencldnfilem  35632  pell1234qrdich  35677  jm2.27  35833  expdiophlem1  35846  wepwsolem  35870  aomclem8  35889  islnr3  35944  lnr2i  35945  lpirlnr  35946  hbtlem1  35952  hbtlem2  35953  hbtlem7  35954  hbtlem4  35955  hbtlem5  35957  hbtlem6  35958  dgraaval  35975  dgraavalOLD  35976  dgraalem  35977  dgraalemOLD  35978  dgraaub  35983  dgraaubOLD  35984  rngunsnply  36009  brtrclfv2  36289  extoimad  36577  elabrexg  37343  foelrnf  37422  disjrnmpt2  37424  upbdrech  37477  ssfiunibd  37481  supxrgere  37510  supxrgelem  37514  supxrge  37515  suplesup  37516  iccshift  37568  iooshift  37572  infrglbOLD  37609  climinf  37624  climinfOLD  37625  climinff  37630  climinffOLD  37631  ellimcabssub0  37637  climf  37642  limcperiod  37648  limclner  37672  cncfshiftioo  37710  fperdvper  37730  itgiccshift  37797  itgperiod  37798  stoweidlem27  37827  stoweidlem31  37832  stoweidlem43  37844  stoweidlem46  37847  stoweidlem52  37853  stoweidlem60  37861  fourierdlem42  37952  fourierdlem42OLD  37953  fourierdlem48  37958  fourierdlem51  37961  fourierdlem54  37964  fourierdlem63  37973  fourierdlem64  37974  fourierdlem65  37975  fourierdlem68  37978  fourierdlem70  37980  fourierdlem71  37981  fourierdlem73  37983  fourierdlem80  37990  fourierdlem81  37991  fourierdlem89  37999  fourierdlem90  38000  fourierdlem91  38001  fourierdlem92  38002  fourierdlem96  38006  fourierdlem97  38007  fourierdlem98  38008  fourierdlem99  38009  fourierdlem100  38010  fourierdlem103  38013  fourierdlem104  38014  fourierdlem105  38015  fourierdlem108  38018  fourierdlem109  38019  fourierdlem110  38020  fourierdlem112  38022  fourierdlem113  38023  sge0pnffigt  38146  sge0resplit  38156  ovnval2  38271  ovnval2b  38278  ovnlecvr  38284  ovnpnfelsup  38285  ovn0lem  38291  ovnsubaddlem1  38296  hoidmvlelem1  38321  ovnhoilem1  38327  ovnhoi  38329  cbvrex2  38465  afvelrnb  38535  afvelrnb0  38536  iccelpart  38617  iccpartiun  38618  icceuelpart  38620  m1expevenALTV  38647  odd2np1ALTV  38673  opoeALTV  38682  opeoALTV  38683  isgbo  38723  isgboa  38724  7gbo  38743  9gboa  38745  11gboa  38746  bgoldbwt  38748  nnsum3primesgbe  38757  nnsum4primesodd  38761  nnsum4primesoddALTV  38762  bgoldbtbnd  38774  cshword2  38848  n0snor2el  38862  usgredg4  39081  usgredg2vtx  39083  usgredgedga  39091  dfnbgr2  39174  nbgrel  39177  nbusgrvtx  39181  nbgrnself  39194  uvtxael1  39227  uvtxa01vtx0  39228  cusgrfilem2  39274  cusgrfi  39276  0nodd  39430  1odd  39431  2nodd  39432  0even  39551  1neven  39552  2even  39553  2zlidl  39554  2zrngamgm  39559  2zrngagrp  39563  2zrngmmgm  39566  2zrngnmrid  39570  lcoval  39827  el0ldep  39881  ldepspr  39888  zlmodzxzldep  39919