Theorem rexbidv 2954

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

Syntax hints:   -> wi 4   <-> wb 184   e. wcel 1804   E.wrex 2794

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691

This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1600  df-rex 2799

This theorem is referenced by:  rexbiiOLD  2956  2rexbidv  2961  rexralbidv  2962  rexeqbi1dv  3049  rexeqbidv  3055  cbvrex2v  3079  rspc2ev  3207  rspc3ev  3209  ceqsrex2v  3221  sbcrexgOLD  3399  uniiunlem  3573  rabasiun  4319  eliun  4320  dfiin2g  4348  dfiunv2  4351  elrnmpt  5239  elrnmptg  5242  elimag  5331  fvelrnb  5905  fvelimab  5914  foelrn  6035  foco2  6036  elabrex  6140  abrexco  6141  f1oiso  6232  f1oiso2  6233  grprinvlem  6498  orduninsuc  6663  funcnvuni  6738  fun11iun  6745  abrexex2g  6762  abrexex2  6766  f1oweALT  6769  el2xptp  6828  recseq  7045  tfrlem12  7060  seqomlem2  7118  nneob  7303  qseq2  7364  elqsg  7365  elixpsn  7510  ixpsnf1o  7511  isfi  7541  enfi  7738  pssnn  7740  frfi  7767  unblem1  7774  unblem2  7775  unbnn2  7779  fofinf1o  7803  finsschain  7829  indexfi  7830  elfi  7875  marypha1lem  7895  supeq3  7911  supmo  7914  suplub  7922  supisolem  7934  oieq1  7940  ordtypelem2  7947  ordtypelem3  7948  ordtypelem9  7954  wemaplem1  7974  brwdom2  8002  brwdom3  8011  unwdomg  8013  oemapval  8105  cantnf  8115  cantnfOLD  8137  wemapwe  8142  wemapweOLD  8143  cnfcom3clem  8152  cnfcom3clemOLD  8160  tz9.13  8212  tz9.13g  8213  cardf2  8327  isnum2  8329  ennum  8331  cardiun  8366  infxpenc2  8402  infxpenc2OLD  8406  aceq1  8501  aceq2  8503  dfac5lem3  8509  dfac5lem4  8510  dfac2a  8513  dfac2  8514  kmlem9  8541  kmlem12  8544  kmlem14  8546  ackbij1  8621  cflm  8633  cfss  8648  cofsmo  8652  cfsmolem  8653  cfcoflem  8655  coftr  8656  isfin7  8684  fin23lem26  8708  isf32lem5  8740  fin1a2lem11  8793  hsmexlem2  8810  axdc3lem3  8835  axdc3  8837  numthcor  8877  zorn2lem7  8885  brdom3  8909  brdom7disj  8912  brdom6disj  8913  iundom2g  8918  fpwwe2  9024  winainflem  9074  winalim2  9077  inar1  9156  tskuni  9164  nqereu  9310  prnmax  9376  genpv  9380  genpnmax  9388  genpass  9390  prlem936  9428  recexsrlem  9483  map2psrpr  9490  supsrlem  9491  axrrecex  9543  axpre-sup  9549  dedekind  9747  cnegex  9764  recex  10188  fimaxre3  10499  infm3  10509  supmul1  10515  supmullem1  10516  supmullem2  10517  supmul  10518  creur  10537  creui  10538  cju  10539  nnunb  10798  arch  10799  xrsupsslem  11509  xrinfmsslem  11510  xrsupss  11511  xrinfmss  11512  xrub  11514  supxrunb1  11522  supxrunb2  11523  infmxrgelb  11537  fsequb2  12068  iswrd  12532  wrdval  12533  csbwrdg  12552  cshword  12744  0csh0  12746  2cshwcshw  12775  scshwfzeqfzo  12776  shftfval  12885  abs1m  13150  rexfiuz  13162  limsupbnd2  13288  clim  13299  rlim  13300  rlim2  13301  rlim0  13313  rlim0lt  13314  ello1mpt2  13327  o1lo1  13342  o1compt  13392  rlimdiv  13450  climsup  13474  sumeq1  13493  sumeq2w  13496  summo  13521  fsum  13524  fsumcvg3  13533  infcvgaux2i  13651  mertenslem1  13675  mertenslem2  13676  mertens  13677  prodeq1f  13697  prodeq2w  13701  prodmo  13725  fprod  13730  divides  13970  odd2np1lem  14027  divalglem4  14036  divalglem10  14042  divalg  14043  gcdcllem3  14133  bezoutlem1  14158  exprmfct  14233  nnnn0modprm0  14313  opeo  14319  omeo  14320  pythagtriplem2  14323  pythagtrip  14340  pceu  14352  pcprmpw2  14387  unbenlem  14408  4sqlem12  14456  vdwapval  14473  vdwapun  14474  vdwmc2  14479  vdwpc  14480  vdwlem2  14482  vdwlem10  14490  vdwlem13  14493  vdwnnlem1  14495  rami  14515  cshwsiun  14566  cshwrepswhash1  14569  brssc  15165  isdrs  15542  drsdir  15543  drsdirfi  15546  isdrs2  15547  ipodrsima  15774  gsumvalx  15876  gsumpropd  15878  gsumress  15882  isnsgrp  15894  sgrp2nmndlem5  16026  grpinvex  16044  grp1  16121  imasgrp2  16164  conjnmzb  16280  gaorb  16324  orbsta  16330  symgfix2  16420  symgextfo  16426  pmtrprfvalrn  16492  psgnunilem3  16500  psgneu  16510  psgnval  16511  psgnvali  16512  psgnvalii  16513  ispgp  16591  subgpgp  16596  sylow1  16602  pgpfi  16604  sylow2blem3  16621  fislw  16624  sylow3lem2  16627  lsmelvalm  16650  lsmass  16667  pj1fval  16691  pj1val  16692  pj1eu  16693  pj1id  16696  efgrelexlema  16746  efgrelexlemb  16747  efgredeu  16749  cyggeninv  16865  cygabl  16872  pgpfac1lem2  17105  pgpfac1lem3  17107  pgpfac1lem4  17108  pgpfac1  17110  pgpfaclem2  17112  pgpfac  17114  dvdsrval  17273  dvdsr  17274  subrgdvds  17422  lss1d  17588  lspsn  17627  lspsnel  17628  lspsolvlem  17767  rspsn  17881  opsrval  18118  znf1o  18568  cygznlem3  18586  psgndiflemA  18615  ellspd  18814  ellspdOLD  18815  mat1dimelbas  18951  mat1dimbas  18952  scmatval  18984  scmatel  18985  scmateALT  18992  mat0scmat  19018  decpmataa0  19247  decpmatmulsumfsupp  19252  pmatcollpw2lem  19256  pm2mpmhmlem1  19297  chpscmat  19321  basis2  19430  eltg2  19437  tg2  19444  isclo  19566  neival  19581  isnei  19582  isneip  19584  restbas  19637  neitr  19659  cnpval  19715  iscnp  19716  cnpimaex  19735  lmbr  19737  lmbr2  19738  cnprest2  19769  lmff  19780  regsep  19813  pnrmopn  19822  nrmsep3  19834  isnrm2  19837  iscmp  19866  cmpsublem  19877  cmpsub  19878  tgcmp  19879  sscmp  19883  hauscmplem  19884  1stcclb  19923  1stcfb  19924  is2ndc  19925  2ndc1stc  19930  1stcrest  19932  2ndcctbss  19934  1stcelcls  19940  llyeq  19949  nllyeq  19950  hausllycmp  19973  lly1stc  19975  refssex  19990  refun0  19994  islocfin  19996  locfinnei  20002  comppfsc  20011  txbas  20046  ptval  20049  ptpjopn  20091  ptclsg  20094  txcnp  20099  ptcnp  20101  txrest  20110  ptrescn  20118  txcmp  20122  tx1stc  20129  xkococn  20139  kqreglem1  20220  fbasssin  20315  fbssfi  20316  fbssint  20317  fbun  20319  fgss2  20353  fgcl  20357  ufli  20393  fmfnfmlem3  20435  fbflim2  20456  hauspwpwf1  20466  flfneii  20471  flftg  20475  txflf  20485  fclscf  20504  alexsubb  20524  alexsubALT  20529  tsmssubm  20622  ustincl  20688  ustdiag  20689  ustinvel  20690  ustexhalf  20691  ust0  20700  trust  20710  elutop  20714  ucnval  20758  ucncn  20766  cfiluexsm  20771  cfiluweak  20776  blssps  20905  blss  20906  imasf1oxms  20970  mopni  20973  metss  20989  metrest  21005  metcnp3  21021  cfilucfilOLD  21050  cfilucfil  21051  metuel2  21060  nlmvscn  21174  nrginvrcn  21178  icccmplem1  21305  icccmplem2  21306  icccmp  21308  divcn  21350  cncfval  21370  elcncf2  21372  cncfmet  21390  cnheibor  21433  evth  21437  lebnumlem3  21441  lebnum  21442  xlebnum  21443  lebnumii  21444  ipcn  21664  lmmbr  21675  lmmbr2  21676  cfilfval  21681  cfili  21685  iscfil3  21690  caufval  21692  iscau  21693  iscau2  21694  equivcfil  21716  equivcau  21717  lmcau  21729  ovolval  21863  elovolm  21864  ovolgelb  21869  ovoliunlem1  21891  ovoliun2  21895  ovolshftlem1  21898  ovolscalem1  21902  ovolicc  21912  ioombl1lem4  21949  uniioombllem2  21970  mbfaddlem  22045  mbfsup  22049  mbfinf  22050  mbflimsup  22051  i1fmulc  22088  itg1climres  22099  itg2val  22113  itg2l  22114  itg2leub  22119  itg2seq  22127  itg2monolem1  22135  itg2mono  22138  itg2i1fseq2  22141  cniccibl  22225  ellimc3  22261  limciun  22276  dvferm1  22364  dvferm2  22366  lhop1lem  22392  ply1divex  22515  ig1peu  22550  plyval  22568  elply2  22571  coeval  22598  coeeu  22600  coelem  22601  coeeq  22602  plydivlem4  22670  plydivex  22671  aannenlem2  22703  aalioulem2  22707  aaliou2  22714  ulmval  22753  ulm2  22758  ulmcau  22768  ulmdvlem3  22775  abelthlem9  22813  abelth  22814  efif1olem4  22910  eflogeq  22964  efopn  23017  cxpcn3  23100  cxpeq  23109  rlimcnp  23273  muval  23384  dchrptlem1  23517  dchrptlem2  23518  lgsdchrval  23600  pntpbnd  23751  pntibndlem3  23755  pntibnd  23756  pntlemi  23767  pntleme  23771  pntlemp  23773  pnt3  23775  istrkgld  23835  axtgsegcon  23839  axtgpasch  23842  axtgcont1  23843  legov  23950  islnopp  24091  ishpg  24106  hpgbr  24107  hpgcom  24114  ttgval  24156  ttgitvval  24163  ttgelitv  24164  brbtwn  24180  brcgr  24181  axpasch  24222  axlowdim2  24241  axlowdim  24242  axcontlem2  24246  axcontlem4  24248  axcontlem7  24251  axcontlem8  24252  nbgraf1olem1  24419  cusgrafilem2  24458  cusgrafi  24460  wwlkn0  24667  clwwlknscsh  24797  erclwwlkneq  24801  eclclwwlkn0  24809  eleclclwwlkn  24811  hashecclwwlkn1  24812  usghashecclwwlk  24813  el2wlksot  24858  el2pthsot  24859  2spot2iun2spont  24869  iseupa  24943  3cyclfrgrarn1  24990  usgn0fidegnn0  25007  frgrancvvdeqlem4  25011  friendshipgt3  25099  isgrpo  25176  isgrpoi  25178  grpoidinvlem3  25186  grpoideu  25189  grpoidinv2  25198  isgrp2d  25215  isgrpda  25277  ghgrpOLD  25348  rngoid  25363  nmoofval  25655  nmooval  25656  nmosetn0  25658  nmoolb  25664  nmoubi  25665  nmlno0lem  25686  chcompl  26138  pjhthmo  26198  pjhval  26293  pjpreeq  26294  h1de2ci  26452  elspansn  26462  nmopval  26753  nmopsetn0  26762  nmfnval  26773  nmfnsetn0  26775  eigvecval  26793  hhcno  26801  hhcnf  26802  nmoplb  26804  nmopub  26805  nmfnlb  26821  nmfnleub  26822  eleigvec  26854  nmlnop0iALT  26892  nmopun  26911  nmcexi  26923  branmfn  27002  pjnmopi  27045  cvbr  27179  hatomic  27257  chrelat2  27267  cdjreui  27329  cdj3lem2  27332  reuxfr4d  27367  elabreximd  27386  br8d  27441  unipreima  27462  abfmpunirn  27468  curry2ima  27504  toslublem  27633  tosglblem  27635  archirng  27710  archiexdiv  27712  archiabllem2a  27716  archiabl  27720  isarchiofld  27785  crefi  27828  pcmplfin  27841  pstmfval  27853  tpr2rico  27872  rge0scvg  27909  ismntop  27982  esumc  28040  esumpcvgval  28062  dya2icoseg2  28227  dya2iocuni  28232  eulerpartlemgvv  28293  eulerpartlemgh  28295  lgamgulmlem6  28554  subfacp1lem3  28604  pconcn  28647  cnpcon  28653  txpcon  28655  conpcon  28658  iscvm  28682  cvmcov  28686  cvmopnlem  28701  cvmliftlem15  28721  cvmlift3lem2  28743  cvmlift3lem4  28745  cvmlift3  28751  br8  29161  br6  29162  br4  29163  dfrdg2  29204  dfrdg3  29205  orderseqlem  29308  poseq  29309  soseq  29310  elno  29382  sltval  29383  nobndlem6  29433  nofulllem1  29438  nofulllem2  29439  nofulllem5  29442  altxpeq2  29600  funtransport  29657  fvtransport  29658  brcolinear2  29684  colineardim1  29687  segcon2  29731  brsegle  29734  funray  29766  fvray  29767  funline  29768  linedegen  29769  fvline  29770  ellines  29778  supaddc  30017  supadd  30018  ptrest  30024  heicant  30025  mblfinlem1  30027  mblfinlem3  30029  mblfinlem4  30030  ismblfin  30031  itg2addnclem  30042  itg2addnclem3  30044  itg2addnc  30045  itg2gt0cn  30046  cnicciblnc  30062  ftc1anclem6  30071  gtinf  30113  nn0prpwlem  30116  fnessref  30151  neibastop2lem  30154  neibastop2  30155  tailfb  30171  unirep  30179  indexa  30200  sdclem2  30211  sdclem1  30212  sdc  30213  fdc  30214  fdc1  30215  incsequz  30217  istotbnd  30241  sstotbnd2  30246  equivtotbnd  30250  isbnd  30252  bndss  30258  ssbnd  30260  totbndbnd  30261  ismtybndlem  30278  heibor1lem  30281  heiborlem1  30283  heiborlem6  30288  heiborlem8  30290  heiborlem10  30292  heibor  30293  isdrngo2  30337  divrngidl  30401  prnc  30440  isfldidl  30441  prtlem5  30573  prtlem13  30585  prtlem16  30586  elrfi  30602  isnacs  30612  nacsfg  30613  nacsfix  30620  mzpcompact2lem  30660  eldiophb  30666  eldioph  30667  eldioph2  30671  eldioph2b  30672  eldioph3  30675  eldiophss  30684  diophrex  30685  sbc2rexgOLD  30697  rexrabdioph  30703  rexfrabdioph  30704  elnn0rabdioph  30712  dvdsrabdioph  30719  eldioph4b  30721  eldioph4i  30722  diophren  30723  rencldnfilem  30730  pell1234qrdich  30773  jm2.27  30926  expdiophlem1  30939  wepwsolem  30963  aomclem8  30983  islnr3  31040  lnr2i  31041  lpirlnr  31042  hbtlem1  31048  hbtlem2  31049  hbtlem7  31050  hbtlem4  31051  hbtlem5  31053  hbtlem6  31054  dgraaval  31069  dgraalem  31070  dgraaub  31073  rngunsnply  31098  elabrexg  31384  upbdrech  31459  ssfiunibd  31463  iccshift  31512  iooshift  31516  infrglb  31538  climinf  31566  climinff  31571  ellimcabssub0  31577  climf  31582  limcperiod  31588  limclner  31611  cncfshiftioo  31649  fperdvper  31669  itgiccshift  31733  itgperiod  31734  stoweidlem27  31763  stoweidlem31  31767  stoweidlem43  31779  stoweidlem46  31782  stoweidlem52  31788  stoweidlem60  31796  fourierdlem42  31885  fourierdlem48  31891  fourierdlem51  31894  fourierdlem54  31897  fourierdlem63  31906  fourierdlem64  31907  fourierdlem65  31908  fourierdlem68  31911  fourierdlem70  31913  fourierdlem71  31914  fourierdlem73  31916  fourierdlem80  31923  fourierdlem81  31924  fourierdlem89  31932  fourierdlem90  31933  fourierdlem91  31934  fourierdlem92  31935  fourierdlem96  31939  fourierdlem97  31940  fourierdlem98  31941  fourierdlem99  31942  fourierdlem100  31943  fourierdlem103  31946  fourierdlem104  31947  fourierdlem105  31948  fourierdlem108  31951  fourierdlem109  31952  fourierdlem110  31953  fourierdlem112  31955  fourierdlem113  31956  etransclem48  32019  cbvrex2  32132  afvelrnb  32202  afvelrnb0  32203  0nodd  32451  1odd  32452  2nodd  32453  0even  32564  1neven  32565  2even  32566  2zlidl  32567  2zrngamgm  32572  2zrngagrp  32576  2zrngmmgm  32579  2zrngnmrid  32583  lcoval  32883  el0ldep  32937  ldepspr  32944  zlmodzxzldep  32975  bnj66  33786  bnj873  33850  bnj18eq1  33853  bnj1234  33937  bnj1318  33949  bj-finsumval0  34538  islshp  34579  lsmsat  34608  lcvbr  34621  lsatcv0  34631  lshpsmreu  34709  lshpkrlem1  34710  lshpkrlem2  34711  lshpkrlem3  34712  lshpkrcl  34716  lshpset2N  34719  islshpkrN  34720  cvrval  34869  atlex  34916  glbconxN  34977  hlsuprexch  34980  islln  35105  islpln  35129  islpln5  35134  lvolex3N  35137  islvol  35172  islvol5  35178  ispointN  35341  pmapglbx  35368  paddval  35397  elpaddn0  35399  elpaddat  35403  elpadd0  35408  4atex  35675  4atex2  35676  cdlemefrs29bpre1  35998  cdlemefrs32fva  36001  cdlemg33b  36308  dvhb1dimN  36587  dvhopellsm  36719  dib1dim  36767  diclspsn  36796  dihglblem2aN  36895  dihglblem2N  36896  dih1dimatlem  36931  dvh3dimatN  37041  dvh2dim  37047  dvh3dim  37048  dvh4dimN  37049  dvh3dim3N  37051  dochfl1  37078  lcfl7N  37103  lcf1o  37153  lcfrlem39  37183  mapdpglem3  37277  hvmapvalvalN  37363  hdmap14lem2a  37472  hdmapglem7a  37532  extoimad  37785