Theorem rexbidv 2973

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

Syntax hints:   -> wi 4   <-> wb 184   e. wcel 1767   E.wrex 2815

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680

This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1597  df-rex 2820

This theorem is referenced by:  rexbiiOLD  2975  2rexbidv  2980  rexralbidv  2981  rexeqbi1dv  3067  rexeqbidv  3073  cbvrex2v  3097  rspc2ev  3225  rspc3ev  3227  ceqsrex2v  3239  sbcrexgOLD  3417  uniiunlem  3588  rabasiun  4329  eliun  4330  dfiin2g  4358  dfiunv2  4361  elrnmpt  5247  elrnmptg  5250  elimag  5339  fvelrnb  5913  fvelimab  5921  foelrn  6038  foco2  6039  elabrex  6141  abrexco  6142  f1oiso  6233  f1oiso2  6234  grprinvlem  6495  orduninsuc  6656  funcnvuni  6734  fun11iun  6741  abrexex2g  6758  abrexex2  6762  f1oweALT  6765  el2xptp  6824  recseq  7040  tfrlem12  7055  seqomlem2  7113  nneob  7298  qseq2  7359  elqsg  7360  elixpsn  7505  ixpsnf1o  7506  isfi  7536  enfi  7733  pssnn  7735  frfi  7761  unblem1  7768  unblem2  7769  unbnn2  7773  fofinf1o  7797  finsschain  7823  indexfi  7824  elfi  7869  marypha1lem  7889  supeq3  7905  supmo  7908  suplub  7916  supisolem  7927  oieq1  7933  ordtypelem2  7940  ordtypelem3  7941  ordtypelem9  7947  wemaplem1  7967  brwdom2  7995  brwdom3  8004  unwdomg  8006  oemapval  8098  cantnf  8108  cantnfOLD  8130  wemapwe  8135  wemapweOLD  8136  cnfcom3clem  8145  cnfcom3clemOLD  8153  tz9.13  8205  tz9.13g  8206  cardf2  8320  isnum2  8322  ennum  8324  cardiun  8359  infxpenc2  8395  infxpenc2OLD  8399  aceq1  8494  aceq2  8496  dfac5lem3  8502  dfac5lem4  8503  dfac2a  8506  dfac2  8507  kmlem9  8534  kmlem12  8537  kmlem14  8539  ackbij1  8614  cflm  8626  cfss  8641  cofsmo  8645  cfsmolem  8646  cfcoflem  8648  coftr  8649  isfin7  8677  fin23lem26  8701  isf32lem5  8733  fin1a2lem11  8786  hsmexlem2  8803  axdc3lem3  8828  axdc3  8830  numthcor  8870  zorn2lem7  8878  brdom3  8902  brdom7disj  8905  brdom6disj  8906  iundom2g  8911  fpwwe2  9017  winainflem  9067  winalim2  9070  inar1  9149  tskuni  9157  nqereu  9303  prnmax  9369  genpv  9373  genpnmax  9381  genpass  9383  prlem936  9421  recexsrlem  9476  map2psrpr  9483  supsrlem  9484  axrrecex  9536  axpre-sup  9542  dedekind  9739  cnegex  9756  recex  10177  fimaxre3  10488  infm3  10498  supmul1  10504  supmullem1  10505  supmullem2  10506  supmul  10507  creur  10526  creui  10527  cju  10528  nnunb  10787  arch  10788  xrsupsslem  11494  xrinfmsslem  11495  xrsupss  11496  xrinfmss  11497  xrub  11499  supxrunb1  11507  supxrunb2  11508  infmxrgelb  11522  fsequb2  12049  iswrd  12510  wrdval  12511  csbwrdg  12530  cshword  12719  0csh0  12721  2cshwcshw  12750  scshwfzeqfzo  12751  shftfval  12860  abs1m  13124  rexfiuz  13136  limsupbnd2  13262  clim  13273  rlim  13274  rlim2  13275  rlim0  13287  rlim0lt  13288  ello1mpt2  13301  o1lo1  13316  o1compt  13366  rlimdiv  13424  climsup  13448  sumeq1  13467  sumeq2w  13470  summo  13495  fsum  13498  fsumcvg3  13507  infcvgaux2i  13625  mertenslem1  13649  mertenslem2  13650  mertens  13651  divides  13842  odd2np1lem  13897  divalglem4  13906  divalglem10  13912  divalg  13913  gcdcllem3  14003  bezoutlem1  14028  exprmfct  14103  nnnn0modprm0  14183  opeo  14189  omeo  14190  pythagtriplem2  14193  pythagtrip  14210  pceu  14222  pcprmpw2  14257  unbenlem  14278  4sqlem12  14326  vdwapval  14343  vdwapun  14344  vdwmc2  14349  vdwpc  14350  vdwlem2  14352  vdwlem10  14360  vdwlem13  14363  vdwnnlem1  14365  rami  14385  cshwsiun  14435  cshwrepswhash1  14438  brssc  15037  isdrs  15414  drsdir  15415  drsdirfi  15418  isdrs2  15419  ipodrsima  15645  gsumvalx  15812  gsumpropd  15814  gsumress  15817  grpinvex  15863  imasgrp2  15982  conjnmzb  16093  gaorb  16137  orbsta  16143  symgfix2  16233  symgextfo  16239  pmtrprfvalrn  16306  psgnunilem3  16314  psgneu  16324  psgnval  16325  psgnvali  16326  psgnvalii  16327  ispgp  16405  subgpgp  16410  sylow1  16416  pgpfi  16418  sylow2blem3  16435  fislw  16438  sylow3lem2  16441  lsmelvalm  16464  lsmass  16481  pj1fval  16505  pj1val  16506  pj1eu  16507  pj1id  16510  efgrelexlema  16560  efgrelexlemb  16561  efgredeu  16563  cyggeninv  16674  cygabl  16681  pgpfac1lem2  16913  pgpfac1lem3  16915  pgpfac1lem4  16916  pgpfac1  16918  pgpfaclem2  16920  pgpfac  16922  dvdsrval  17075  dvdsr  17076  subrgdvds  17223  lss1d  17389  lspsn  17428  lspsnel  17429  lspsolvlem  17568  rspsn  17681  opsrval  17907  znf1o  18354  cygznlem3  18372  psgndiflemA  18401  ellspd  18600  ellspdOLD  18601  mat1dimelbas  18737  mat1dimbas  18738  scmatval  18770  scmatel  18771  scmateALT  18778  mat0scmat  18804  decpmataa0  19033  decpmatmulsumfsupp  19038  pmatcollpw2lem  19042  pm2mpmhmlem1  19083  chpscmat  19107  basis2  19216  eltg2  19223  tg2  19230  isclo  19351  neival  19366  isnei  19367  isneip  19369  restbas  19422  neitr  19444  cnpval  19500  iscnp  19501  cnpimaex  19520  lmbr  19522  lmbr2  19523  cnprest2  19554  lmff  19565  regsep  19598  pnrmopn  19607  nrmsep3  19619  isnrm2  19622  iscmp  19651  cmpsublem  19662  cmpsub  19663  tgcmp  19664  sscmp  19668  hauscmplem  19669  1stcclb  19708  1stcfb  19709  is2ndc  19710  2ndc1stc  19715  1stcrest  19717  2ndcctbss  19719  1stcelcls  19725  llyeq  19734  nllyeq  19735  hausllycmp  19758  lly1stc  19760  txbas  19800  ptval  19803  ptpjopn  19845  ptclsg  19848  txcnp  19853  ptcnp  19855  txrest  19864  ptrescn  19872  txcmp  19876  tx1stc  19883  xkococn  19893  kqreglem1  19974  fbasssin  20069  fbssfi  20070  fbssint  20071  fbun  20073  fgss2  20107  fgcl  20111  ufli  20147  fmfnfmlem3  20189  fbflim2  20210  hauspwpwf1  20220  flfneii  20225  flftg  20229  txflf  20239  fclscf  20258  alexsubb  20278  alexsubALT  20283  tsmssubm  20376  ustincl  20442  ustdiag  20443  ustinvel  20444  ustexhalf  20445  ust0  20454  trust  20464  elutop  20468  ucnval  20512  ucncn  20520  cfiluexsm  20525  cfiluweak  20530  blssps  20659  blss  20660  imasf1oxms  20724  mopni  20727  metss  20743  metrest  20759  metcnp3  20775  cfilucfilOLD  20804  cfilucfil  20805  metuel2  20814  nlmvscn  20928  nrginvrcn  20932  icccmplem1  21059  icccmplem2  21060  icccmp  21062  divcn  21104  cncfval  21124  elcncf2  21126  cncfmet  21144  cnheibor  21187  evth  21191  lebnumlem3  21195  lebnum  21196  xlebnum  21197  lebnumii  21198  ipcn  21418  lmmbr  21429  lmmbr2  21430  cfilfval  21435  cfili  21439  iscfil3  21444  caufval  21446  iscau  21447  iscau2  21448  equivcfil  21470  equivcau  21471  lmcau  21483  ovolval  21617  elovolm  21618  ovolgelb  21623  ovoliunlem1  21645  ovoliun2  21649  ovolshftlem1  21652  ovolscalem1  21656  ovolicc  21666  ioombl1lem4  21703  uniioombllem2  21724  mbfaddlem  21799  mbfsup  21803  mbfinf  21804  mbflimsup  21805  i1fmulc  21842  itg1climres  21853  itg2val  21867  itg2l  21868  itg2leub  21873  itg2seq  21881  itg2monolem1  21889  itg2mono  21892  itg2i1fseq2  21895  cniccibl  21979  ellimc3  22015  limciun  22030  dvferm1  22118  dvferm2  22120  lhop1lem  22146  ply1divex  22269  ig1peu  22304  plyval  22322  elply2  22325  coeval  22352  coeeu  22354  coelem  22355  coeeq  22356  plydivlem4  22423  plydivex  22424  aannenlem2  22456  aalioulem2  22460  aaliou2  22467  ulmval  22506  ulm2  22511  ulmcau  22521  ulmdvlem3  22528  abelthlem9  22566  abelth  22567  efif1olem4  22662  eflogeq  22711  efopn  22764  cxpcn3  22847  cxpeq  22856  rlimcnp  23020  muval  23131  dchrptlem1  23264  dchrptlem2  23265  lgsdchrval  23347  pntpbnd  23498  pntibndlem3  23502  pntibnd  23503  pntlemi  23514  pntleme  23518  pntlemp  23520  pnt3  23522  istrkgld  23582  axtgsegcon  23586  axtgpasch  23589  axtgcont1  23590  legov  23696  ttgval  23851  ttgitvval  23858  ttgelitv  23859  brbtwn  23875  brcgr  23876  axpasch  23917  axlowdim2  23936  axlowdim  23937  axcontlem2  23941  axcontlem4  23943  axcontlem7  23946  axcontlem8  23947  nbgraf1olem1  24114  cusgrafilem2  24153  cusgrafi  24155  wwlkn0  24362  clwwlknscsh  24492  erclwwlkneq  24496  eclclwwlkn0  24504  eleclclwwlkn  24506  hashecclwwlkn1  24507  usghashecclwwlk  24508  el2wlksot  24553  el2pthsot  24554  2wot2wont  24559  2spot2iun2spont  24564  iseupa  24638  3cyclfrgrarn1  24685  usgn0fidegnn0  24703  frgrancvvdeqlem4  24707  friendshipgt3  24795  isgrpo  24871  isgrpoi  24873  grpoidinvlem3  24881  grpoideu  24884  grpoidinv2  24893  isgrp2d  24910  isgrpda  24972  ghgrp  25043  rngoid  25058  nmoofval  25350  nmooval  25351  nmosetn0  25353  nmoolb  25359  nmoubi  25360  nmlno0lem  25381  chcompl  25833  pjhthmo  25893  pjhval  25988  pjpreeq  25989  h1de2ci  26147  elspansn  26157  nmopval  26448  nmopsetn0  26457  nmfnval  26468  nmfnsetn0  26470  eigvecval  26488  hhcno  26496  hhcnf  26497  nmoplb  26499  nmopub  26500  nmfnlb  26516  nmfnleub  26517  eleigvec  26549  nmlnop0iALT  26587  nmopun  26606  nmcexi  26618  branmfn  26697  pjnmopi  26740  cvbr  26874  hatomic  26952  chrelat2  26962  cdjreui  27024  cdj3lem2  27027  reuxfr4d  27062  elabreximd  27079  br8d  27133  unipreima  27153  abfmpunirn  27159  curry2ima  27195  toslublem  27314  tosglblem  27316  archirng  27391  archiexdiv  27393  archiabllem2a  27397  archiabl  27401  isarchiofld  27467  pstmfval  27508  tpr2rico  27527  rge0scvg  27564  ismntop  27641  esumc  27699  esumpcvgval  27721  dya2icoseg2  27886  dya2iocuni  27891  eulerpartlemgvv  27952  eulerpartlemgh  27954  lgamgulmlem6  28213  subfacp1lem3  28263  pconcn  28306  cnpcon  28312  txpcon  28314  conpcon  28317  iscvm  28341  cvmcov  28345  cvmopnlem  28360  cvmliftlem15  28380  cvmlift3lem2  28402  cvmlift3lem4  28404  cvmlift3  28410  prodeq1f  28614  prodeq2w  28618  prodmo  28642  fprod  28647  br8  28759  br6  28760  br4  28761  dfrdg2  28802  dfrdg3  28803  orderseqlem  28906  poseq  28907  soseq  28908  elno  28980  sltval  28981  nobndlem6  29031  nofulllem1  29036  nofulllem2  29037  nofulllem5  29040  altxpeq2  29198  funtransport  29255  fvtransport  29256  brcolinear2  29282  colineardim1  29285  segcon2  29329  brsegle  29332  funray  29364  fvray  29365  funline  29366  linedegen  29367  fvline  29368  ellines  29376  supaddc  29615  supadd  29616  ptrest  29623  heicant  29624  mblfinlem1  29626  mblfinlem3  29628  mblfinlem4  29629  ismblfin  29630  itg2addnclem  29641  itg2addnclem3  29643  itg2addnc  29644  itg2gt0cn  29645  cnicciblnc  29661  ftc1anclem6  29670  gtinf  29712  nn0prpwlem  29715  refssex  29751  fnessref  29763  islocfin  29766  locfinnei  29772  comppfsc  29777  neibastop2lem  29779  neibastop2  29780  tailfb  29796  unirep  29804  indexa  29825  sdclem2  29836  sdclem1  29837  sdc  29838  fdc  29839  fdc1  29840  incsequz  29842  istotbnd  29866  sstotbnd2  29871  equivtotbnd  29875  isbnd  29877  bndss  29883  ssbnd  29885  totbndbnd  29886  ismtybndlem  29903  heibor1lem  29906  heiborlem1  29908  heiborlem6  29913  heiborlem8  29915  heiborlem10  29917  heibor  29918  isdrngo2  29962  divrngidl  30026  prnc  30065  isfldidl  30066  prtlem5  30199  prtlem13  30211  prtlem16  30212  elrfi  30228  isnacs  30238  nacsfg  30239  nacsfix  30246  mzpcompact2lem  30286  eldiophb  30292  eldioph  30293  eldioph2  30297  eldioph2b  30298  eldioph3  30301  eldiophss  30310  diophrex  30311  sbc2rexgOLD  30323  rexrabdioph  30329  rexfrabdioph  30330  elnn0rabdioph  30338  dvdsrabdioph  30345  eldioph4b  30347  eldioph4i  30348  diophren  30349  rencldnfilem  30356  pell1234qrdich  30399  jm2.27  30554  expdiophlem1  30567  wepwsolem  30591  aomclem8  30611  islnr3  30668  lnr2i  30669  lpirlnr  30670  hbtlem1  30676  hbtlem2  30677  hbtlem7  30678  hbtlem4  30679  hbtlem5  30681  hbtlem6  30682  dgraaval  30698  dgraalem  30699  dgraaub  30702  rngunsnply  30727  elabrexg  31012  upbdrech  31082  ssfiunibd  31086  iccshift  31122  iooshift  31126  infrglb  31140  climinf  31148  climinff  31153  ellimcabssub0  31159  climf  31164  limcperiod  31170  limcleqr  31186  addlimc  31190  0ellimcdiv  31191  limclner  31193  cncfshift  31212  cncfperiod  31217  cncfshiftioo  31231  fperdvper  31248  ioodvbdlimc1lem1  31261  itgiccshift  31298  itgperiod  31299  stoweidlem27  31327  stoweidlem31  31331  stoweidlem43  31343  stoweidlem46  31346  stoweidlem52  31352  stoweidlem60  31360  fourierdlem42  31449  fourierdlem45  31452  fourierdlem48  31455  fourierdlem51  31458  fourierdlem54  31461  fourierdlem63  31470  fourierdlem64  31471  fourierdlem65  31472  fourierdlem68  31475  fourierdlem70  31477  fourierdlem71  31478  fourierdlem73  31480  fourierdlem80  31487  fourierdlem81  31488  fourierdlem87  31494  fourierdlem89  31496  fourierdlem90  31497  fourierdlem91  31498  fourierdlem92  31499  fourierdlem96  31503  fourierdlem97  31504  fourierdlem98  31505  fourierdlem99  31506  fourierdlem100  31507  fourierdlem103  31510  fourierdlem104  31511  fourierdlem105  31512  fourierdlem108  31515  fourierdlem109  31516  fourierdlem110  31517  fourierdlem112  31519  fourierdlem113  31520  cbvrex2  31645  afvelrnb  31715  afvelrnb0  31716  lcoval  32086  el0ldep  32140  ldepspr  32147  grp1  32162  zlmodzxzldep  32186  bnj66  32997  bnj873  33061  bnj18eq1  33064  bnj1234  33148  bnj1318  33160  bj-finsumval0  33735  islshp  33776  lsmsat  33805  lcvbr  33818  lsatcv0  33828  lshpsmreu  33906  lshpkrlem1  33907  lshpkrlem2  33908  lshpkrlem3  33909  lshpkrcl  33913  lshpset2N  33916  islshpkrN  33917  cvrval  34066  atlex  34113  glbconxN  34174  hlsuprexch  34177  islln  34302  islpln  34326  islpln5  34331  lvolex3N  34334  islvol  34369  islvol5  34375  ispointN  34538  pmapglbx  34565  paddval  34594  elpaddn0  34596  elpaddat  34600  elpadd0  34605  4atex  34872  4atex2  34873  cdlemefrs29bpre1  35193  cdlemefrs32fva  35196  cdlemg33b  35503  dvhb1dimN  35782  dvhopellsm  35914  dib1dim  35962  diclspsn  35991  dihglblem2aN  36090  dihglblem2N  36091  dih1dimatlem  36126  dvh3dimatN  36236  dvh2dim  36242  dvh3dim  36243  dvh4dimN  36244  dvh3dim3N  36246  dochfl1  36273  lcfl7N  36298  lcf1o  36348  lcfrlem39  36378  mapdpglem3  36472  hvmapvalvalN  36558  hdmap14lem2a  36667  hdmapglem7a  36727