Theorem rexbidv 2893

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

Syntax hints:   -> wi 4   <-> wb 184   e. wcel 1826   E.wrex 2733

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1626  ax-4 1639  ax-5 1712

This theorem depends on definitions:  df-bi 185  df-an 369  df-ex 1621  df-rex 2738

This theorem is referenced by:  rexbiiOLD  2895  2rexbidv  2900  rexralbidv  2901  rexeqbi1dv  2988  rexeqbidv  2994  cbvrex2v  3018  rspc2ev  3146  rspc3ev  3148  ceqsrex2v  3160  uniiunlem  3502  rabasiun  4247  eliun  4248  dfiin2g  4276  dfiunv2  4279  elrnmpt  5162  elrnmptg  5165  elimag  5253  fvelrnb  5821  fvelimab  5830  foelrn  5952  foco2  5953  elabrex  6056  abrexco  6057  f1oiso  6148  f1oiso2  6149  grprinvlem  6412  orduninsuc  6577  funcnvuni  6652  fun11iun  6659  abrexex2g  6676  abrexex2  6680  f1oweALT  6683  el2xptp  6742  recseq  6961  tfrlem12  6976  seqomlem2  7034  nneob  7219  qseq2  7280  elqsg  7281  elixpsn  7427  ixpsnf1o  7428  isfi  7458  enfi  7652  pssnn  7654  frfi  7680  unblem1  7687  unblem2  7688  unbnn2  7692  fofinf1o  7716  finsschain  7742  indexfi  7743  elfi  7788  marypha1lem  7808  supeq3  7823  supmo  7826  suplub  7834  supisolem  7846  oieq1  7852  ordtypelem2  7859  ordtypelem3  7860  ordtypelem9  7866  wemaplem1  7886  brwdom2  7914  brwdom3  7923  unwdomg  7925  oemapval  8015  cantnf  8025  cantnfOLD  8047  wemapwe  8052  wemapweOLD  8053  cnfcom3clem  8062  cnfcom3clemOLD  8070  tz9.13  8122  tz9.13g  8123  cardf2  8237  isnum2  8239  ennum  8241  cardiun  8276  infxpenc2  8312  infxpenc2OLD  8316  aceq1  8411  aceq2  8413  dfac5lem3  8419  dfac5lem4  8420  dfac2a  8423  dfac2  8424  kmlem9  8451  kmlem12  8454  kmlem14  8456  ackbij1  8531  cflm  8543  cfss  8558  cofsmo  8562  cfsmolem  8563  cfcoflem  8565  coftr  8566  isfin7  8594  fin23lem26  8618  isf32lem5  8650  fin1a2lem11  8703  hsmexlem2  8720  axdc3lem3  8745  axdc3  8747  numthcor  8787  zorn2lem7  8795  brdom3  8819  brdom7disj  8822  brdom6disj  8823  iundom2g  8828  fpwwe2  8932  winainflem  8982  winalim2  8985  inar1  9064  tskuni  9072  nqereu  9218  prnmax  9284  genpv  9288  genpnmax  9296  genpass  9298  prlem936  9336  recexsrlem  9391  map2psrpr  9398  supsrlem  9399  axrrecex  9451  axpre-sup  9457  dedekind  9655  cnegex  9672  recex  10098  fimaxre3  10408  infm3  10418  supmul1  10424  supmullem1  10425  supmullem2  10426  supmul  10427  creur  10446  creui  10447  cju  10448  nnunb  10708  arch  10709  xrsupsslem  11419  xrinfmsslem  11420  xrsupss  11421  xrinfmss  11422  xrub  11424  supxrunb1  11432  supxrunb2  11433  infmxrgelb  11447  fsequb2  11989  iswrd  12454  iswrdOLD  12455  wrdval  12456  csbwrdg  12478  cshword  12673  0csh0  12675  2cshwcshw  12704  scshwfzeqfzo  12705  shftfval  12905  abs1m  13170  rexfiuz  13182  limsupbnd2  13308  clim  13319  rlim  13320  rlim2  13321  rlim0  13333  rlim0lt  13334  ello1mpt2  13347  o1lo1  13362  o1compt  13412  rlimdiv  13470  climsup  13494  sumeq1  13513  sumeq2w  13516  summo  13541  fsum  13544  fsumcvg3  13553  infcvgaux2i  13671  mertenslem1  13695  mertenslem2  13696  mertens  13697  prodeq1f  13717  prodeq2w  13721  prodmo  13745  fprod  13750  divides  13990  odd2np1lem  14047  divalglem4  14056  divalglem10  14062  divalg  14063  gcdcllem3  14153  bezoutlem1  14178  exprmfct  14253  nnnn0modprm0  14333  opeo  14339  omeo  14340  pythagtriplem2  14343  pythagtrip  14360  pceu  14372  pcprmpw2  14407  unbenlem  14428  4sqlem12  14476  vdwapval  14493  vdwapun  14494  vdwmc2  14499  vdwpc  14500  vdwlem2  14502  vdwlem10  14510  vdwlem13  14513  vdwnnlem1  14515  rami  14535  cshwsiun  14586  cshwrepswhash1  14589  brssc  15220  isdrs  15680  drsdir  15681  drsdirfi  15684  isdrs2  15685  ipodrsima  15912  gsumvalx  16014  gsumpropd  16016  gsumress  16020  isnsgrp  16032  sgrp2nmndlem5  16164  grpinvex  16182  grp1  16259  imasgrp2  16302  conjnmzb  16418  gaorb  16462  orbsta  16468  symgfix2  16558  symgextfo  16564  pmtrprfvalrn  16630  psgnunilem3  16638  psgneu  16648  psgnval  16649  psgnvali  16650  psgnvalii  16651  ispgp  16729  subgpgp  16734  sylow1  16740  pgpfi  16742  sylow2blem3  16759  fislw  16762  sylow3lem2  16765  lsmelvalm  16788  lsmass  16805  pj1fval  16829  pj1val  16830  pj1eu  16831  pj1id  16834  efgrelexlema  16884  efgrelexlemb  16885  efgredeu  16887  cyggeninv  17003  cygabl  17010  pgpfac1lem2  17239  pgpfac1lem3  17241  pgpfac1lem4  17242  pgpfac1  17244  pgpfaclem2  17246  pgpfac  17248  dvdsrval  17407  dvdsr  17408  subrgdvds  17556  lss1d  17722  lspsn  17761  lspsnel  17762  lspsolvlem  17901  rspsn  18015  opsrval  18252  znf1o  18681  cygznlem3  18699  psgndiflemA  18728  ellspd  18922  mat1dimelbas  19058  mat1dimbas  19059  scmatval  19091  scmatel  19092  scmateALT  19099  mat0scmat  19125  decpmataa0  19354  decpmatmulsumfsupp  19359  pmatcollpw2lem  19363  pm2mpmhmlem1  19404  chpscmat  19428  basis2  19537  eltg2  19544  tg2  19551  isclo  19674  neival  19689  isnei  19690  isneip  19692  restbas  19745  neitr  19767  cnpval  19823  iscnp  19824  cnpimaex  19843  lmbr  19845  lmbr2  19846  cnprest2  19877  lmff  19888  regsep  19921  pnrmopn  19930  nrmsep3  19942  isnrm2  19945  iscmp  19974  cmpsublem  19985  cmpsub  19986  tgcmp  19987  sscmp  19991  hauscmplem  19992  1stcclb  20030  1stcfb  20031  is2ndc  20032  2ndc1stc  20037  1stcrest  20039  2ndcctbss  20041  1stcelcls  20047  llyeq  20056  nllyeq  20057  hausllycmp  20080  lly1stc  20082  refssex  20097  refun0  20101  islocfin  20103  locfinnei  20109  comppfsc  20118  txbas  20153  ptval  20156  ptpjopn  20198  ptclsg  20201  txcnp  20206  ptcnp  20208  txrest  20217  ptrescn  20225  txcmp  20229  tx1stc  20236  xkococn  20246  kqreglem1  20327  fbasssin  20422  fbssfi  20423  fbssint  20424  fbun  20426  fgss2  20460  fgcl  20464  ufli  20500  fmfnfmlem3  20542  fbflim2  20563  hauspwpwf1  20573  flfneii  20578  flftg  20582  txflf  20592  fclscf  20611  alexsubb  20631  alexsubALT  20636  tsmssubm  20729  ustincl  20795  ustdiag  20796  ustinvel  20797  ustexhalf  20798  ust0  20807  trust  20817  elutop  20821  ucnval  20865  ucncn  20873  cfiluexsm  20878  cfiluweak  20883  blssps  21012  blss  21013  imasf1oxms  21077  mopni  21080  metss  21096  metrest  21112  metcnp3  21128  cfilucfilOLD  21157  cfilucfil  21158  metuel2  21167  nlmvscn  21281  nrginvrcn  21285  icccmplem1  21412  icccmplem2  21413  icccmp  21415  divcn  21457  cncfval  21477  elcncf2  21479  cncfmet  21497  cnheibor  21540  evth  21544  lebnumlem3  21548  lebnum  21549  xlebnum  21550  lebnumii  21551  ipcn  21771  lmmbr  21782  lmmbr2  21783  cfilfval  21788  cfili  21792  iscfil3  21797  caufval  21799  iscau  21800  iscau2  21801  equivcfil  21823  equivcau  21824  lmcau  21836  ovolval  21970  elovolm  21971  ovolgelb  21976  ovoliunlem1  21998  ovoliun2  22002  ovolshftlem1  22005  ovolscalem1  22009  ovolicc  22019  ioombl1lem4  22056  uniioombllem2  22077  mbfaddlem  22152  mbfsup  22156  mbfinf  22157  mbflimsup  22158  i1fmulc  22195  itg1climres  22206  itg2val  22220  itg2l  22221  itg2leub  22226  itg2seq  22234  itg2monolem1  22242  itg2mono  22245  itg2i1fseq2  22248  cniccibl  22332  ellimc3  22368  limciun  22383  dvferm1  22471  dvferm2  22473  lhop1lem  22499  ply1divex  22622  ig1peu  22657  plyval  22675  elply2  22678  coeval  22705  coeeu  22707  coelem  22708  coeeq  22709  plydivlem4  22777  plydivex  22778  aannenlem2  22810  aalioulem2  22814  aaliou2  22821  ulmval  22860  ulm2  22865  ulmcau  22875  ulmdvlem3  22882  abelthlem9  22920  abelth  22921  efif1olem4  23017  eflogeq  23074  efopn  23126  cxpcn3  23209  cxpeq  23218  rlimcnp  23412  muval  23523  dchrptlem1  23656  dchrptlem2  23657  lgsdchrval  23739  pntpbnd  23890  pntibndlem3  23894  pntibnd  23895  pntlemi  23906  pntleme  23910  pntlemp  23912  pnt3  23914  istrkgld  23974  axtgsegcon  23978  axtgpasch  23981  axtgcont1  23982  legov  24092  islnopp  24233  ishpg  24248  hpgbr  24249  hpgcom  24256  ttgval  24299  ttgitvval  24306  ttgelitv  24307  brbtwn  24323  brcgr  24324  axpasch  24365  axlowdim2  24384  axlowdim  24385  axcontlem2  24389  axcontlem4  24391  axcontlem7  24394  axcontlem8  24395  nbgraf1olem1  24562  cusgrafilem2  24601  cusgrafi  24603  wwlkn0  24810  clwwlknscsh  24940  erclwwlkneq  24944  eclclwwlkn0  24952  eleclclwwlkn  24954  hashecclwwlkn1  24955  usghashecclwwlk  24956  el2wlksot  25001  el2pthsot  25002  2spot2iun2spont  25012  iseupa  25086  3cyclfrgrarn1  25133  usgn0fidegnn0  25150  frgrancvvdeqlem4  25154  friendshipgt3  25242  isgrpo  25315  isgrpoi  25317  grpoidinvlem3  25325  grpoideu  25328  grpoidinv2  25337  isgrp2d  25354  isgrpda  25416  ghgrpOLD  25487  rngoid  25502  nmoofval  25794  nmooval  25795  nmosetn0  25797  nmoolb  25803  nmoubi  25804  nmlno0lem  25825  chcompl  26277  pjhthmo  26337  pjhval  26432  pjpreeq  26433  h1de2ci  26591  elspansn  26601  nmopval  26891  nmopsetn0  26900  nmfnval  26911  nmfnsetn0  26913  eigvecval  26931  hhcno  26939  hhcnf  26940  nmoplb  26942  nmopub  26943  nmfnlb  26959  nmfnleub  26960  eleigvec  26992  nmlnop0iALT  27030  nmopun  27049  nmcexi  27061  branmfn  27140  pjnmopi  27183  cvbr  27317  hatomic  27395  chrelat2  27405  cdjreui  27467  cdj3lem2  27470  reuxfr4d  27506  elabreximd  27526  br8d  27597  unipreima  27624  abfmpunirn  27630  curry2ima  27674  toslublem  27808  tosglblem  27810  archirng  27885  archiexdiv  27887  archiabllem2a  27891  archiabl  27895  isarchiofld  27961  crefi  28004  pcmplfin  28017  pstmfval  28029  tpr2rico  28048  rge0scvg  28085  ismntop  28157  esumc  28199  esumpcvgval  28226  esum2dlem  28240  dya2icoseg2  28405  dya2iocuni  28410  eulerpartlemgvv  28498  eulerpartlemgh  28500  lgamgulmlem6  28765  subfacp1lem3  28815  pconcn  28858  cnpcon  28864  txpcon  28866  conpcon  28869  iscvm  28893  cvmcov  28897  cvmopnlem  28912  cvmliftlem15  28932  cvmlift3lem2  28954  cvmlift3lem4  28956  cvmlift3  28962  br8  29351  br6  29352  br4  29353  dfrdg2  29393  dfrdg3  29394  orderseqlem  29497  poseq  29498  soseq  29499  elno  29571  sltval  29572  nobndlem6  29622  nofulllem1  29627  nofulllem2  29628  nofulllem5  29631  altxpeq2  29777  funtransport  29834  fvtransport  29835  brcolinear2  29861  colineardim1  29864  segcon2  29908  brsegle  29911  funray  29943  fvray  29944  funline  29945  linedegen  29946  fvline  29947  ellines  29955  supaddc  30206  supadd  30207  ptrest  30213  heicant  30214  mblfinlem1  30216  mblfinlem3  30218  mblfinlem4  30219  ismblfin  30220  itg2addnclem  30232  itg2addnclem3  30234  itg2addnc  30235  itg2gt0cn  30236  cnicciblnc  30252  ftc1anclem6  30261  gtinf  30303  nn0prpwlem  30306  fnessref  30341  neibastop2lem  30344  neibastop2  30345  tailfb  30361  unirep  30369  indexa  30390  sdclem2  30401  sdclem1  30402  sdc  30403  fdc  30404  fdc1  30405  incsequz  30407  istotbnd  30431  sstotbnd2  30436  equivtotbnd  30440  isbnd  30442  bndss  30448  ssbnd  30450  totbndbnd  30451  ismtybndlem  30468  heibor1lem  30471  heiborlem1  30473  heiborlem6  30478  heiborlem8  30480  heiborlem10  30482  heibor  30483  isdrngo2  30527  divrngidl  30591  prnc  30630  isfldidl  30631  prtlem5  30763  prtlem13  30775  prtlem16  30776  elrfi  30792  isnacs  30802  nacsfg  30803  nacsfix  30810  mzpcompact2lem  30849  eldiophb  30855  eldioph  30856  eldioph2  30860  eldioph2b  30861  eldioph3  30864  eldiophss  30873  diophrex  30874  sbcrexgOLD  30884  sbc2rexgOLD  30887  rexrabdioph  30893  rexfrabdioph  30894  elnn0rabdioph  30902  dvdsrabdioph  30909  eldioph4b  30910  eldioph4i  30911  diophren  30912  rencldnfilem  30919  pell1234qrdich  30962  jm2.27  31116  expdiophlem1  31129  wepwsolem  31153  aomclem8  31173  islnr3  31232  lnr2i  31233  lpirlnr  31234  hbtlem1  31240  hbtlem2  31241  hbtlem7  31242  hbtlem4  31243  hbtlem5  31245  hbtlem6  31246  dgraaval  31261  dgraalem  31262  dgraaub  31265  rngunsnply  31290  elabrexg  31597  upbdrech  31671  ssfiunibd  31675  iccshift  31724  iooshift  31728  infrglb  31750  climinf  31778  climinff  31783  ellimcabssub0  31789  climf  31794  limcperiod  31800  limclner  31823  cncfshiftioo  31861  fperdvper  31881  itgiccshift  31945  itgperiod  31946  stoweidlem27  31975  stoweidlem31  31979  stoweidlem43  31991  stoweidlem46  31994  stoweidlem52  32000  stoweidlem60  32008  fourierdlem42  32097  fourierdlem48  32103  fourierdlem51  32106  fourierdlem54  32109  fourierdlem63  32118  fourierdlem64  32119  fourierdlem65  32120  fourierdlem68  32123  fourierdlem70  32125  fourierdlem71  32126  fourierdlem73  32128  fourierdlem80  32135  fourierdlem81  32136  fourierdlem89  32144  fourierdlem90  32145  fourierdlem91  32146  fourierdlem92  32147  fourierdlem96  32151  fourierdlem97  32152  fourierdlem98  32153  fourierdlem99  32154  fourierdlem100  32155  fourierdlem103  32158  fourierdlem104  32159  fourierdlem105  32160  fourierdlem108  32163  fourierdlem109  32164  fourierdlem110  32165  fourierdlem112  32167  fourierdlem113  32168  cbvrex2  32344  afvelrnb  32414  afvelrnb0  32415  m1expevenALTV  32490  odd2np1ALTV  32516  opoeALTV  32525  opeoALTV  32526  cshword2  32612  0nodd  32816  1odd  32817  2nodd  32818  0even  32937  1neven  32938  2even  32939  2zlidl  32940  2zrngamgm  32945  2zrngagrp  32949  2zrngmmgm  32952  2zrngnmrid  32956  lcoval  33213  el0ldep  33267  ldepspr  33274  zlmodzxzldep  33305  bnj66  34265  bnj873  34329  bnj18eq1  34332  bnj1234  34416  bnj1318  34428  bj-finsumval0  35010  islshp  35117  lsmsat  35146  lcvbr  35159  lsatcv0  35169  lshpsmreu  35247  lshpkrlem1  35248  lshpkrlem2  35249  lshpkrlem3  35250  lshpkrcl  35254  lshpset2N  35257  islshpkrN  35258  cvrval  35407  atlex  35454  glbconxN  35515  hlsuprexch  35518  islln  35643  islpln  35667  islpln5  35672  lvolex3N  35675  islvol  35710  islvol5  35716  ispointN  35879  pmapglbx  35906  paddval  35935  elpaddn0  35937  elpaddat  35941  elpadd0  35946  4atex  36213  4atex2  36214  cdlemefrs29bpre1  36536  cdlemefrs32fva  36539  cdlemg33b  36846  dvhb1dimN  37125  dvhopellsm  37257  dib1dim  37305  diclspsn  37334  dihglblem2aN  37433  dihglblem2N  37434  dih1dimatlem  37469  dvh3dimatN  37579  dvh2dim  37585  dvh3dim  37586  dvh4dimN  37587  dvh3dim3N  37589  dochfl1  37616  lcfl7N  37641  lcf1o  37691  lcfrlem39  37721  mapdpglem3  37815  hvmapvalvalN  37901  hdmap14lem2a  38010  hdmapglem7a  38070  brtrclfv2  38258  extoimad  38510