Theorem rexbidv 3052

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

Syntax hints:   -> wi 4   <-> wb 196   e. wcel 1990   E.wrex 2913

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839

This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1705  df-rex 2918

This theorem is referenced by:  2rexbidv  3057  rexralbidv  3058  rexeqbi1dv  3147  rexeqbidv  3153  cbvrex2v  3180  rspc2ev  3324  rspc3ev  3326  ceqsrex2v  3338  uniiunlem  3691  n0snor2el  4364  eliun  4524  dfiin2g  4553  dfiunv2  4556  elrnmpt  5372  elrnmptg  5375  elimag  5470  fvelrnb  6243  fvelimab  6253  foelrn  6378  foco2  6379  foco2OLD  6380  elabrex  6501  abrexco  6502  f1oiso  6601  f1oiso2  6602  grprinvlem  6872  orduninsuc  7043  funcnvuni  7119  fun11iun  7126  abrexex2g  7144  abrexex2OLD  7150  f1oweALT  7152  el2xptp  7211  tfrlem12  7485  seqomlem2  7546  nneob  7732  qseq2  7797  elqsg  7798  elqsecl  7801  elixpsn  7947  ixpsnf1o  7948  isfi  7979  enfi  8176  pssnn  8178  frfi  8205  unblem1  8212  unblem2  8213  unbnn2  8217  fofinf1o  8241  finsschain  8273  indexfi  8274  elfi  8319  marypha1lem  8339  supeq3  8355  supmo  8358  suplub  8366  supisolem  8379  eqinf  8390  infval  8392  infglb  8396  infglbb  8397  infmo  8401  oieq1  8417  ordtypelem2  8424  ordtypelem3  8425  ordtypelem9  8431  wemaplem1  8451  brwdom2  8478  brwdom3  8487  unwdomg  8489  oemapval  8580  cantnf  8590  wemapwe  8594  cnfcom3clem  8602  tz9.13  8654  tz9.13g  8655  cardf2  8769  isnum2  8771  ennum  8773  cardiun  8808  infxpenc2  8845  aceq1  8940  aceq2  8942  dfac5lem3  8948  dfac5lem4  8949  dfac2a  8952  dfac2  8953  kmlem9  8980  kmlem12  8983  kmlem14  8985  ackbij1  9060  cflm  9072  cfss  9087  cofsmo  9091  cfsmolem  9092  cfcoflem  9094  coftr  9095  isfin7  9123  fin23lem26  9147  isf32lem5  9179  fin1a2lem11  9232  hsmexlem2  9249  axdc3lem3  9274  axdc3  9276  numthcor  9316  zorn2lem7  9324  brdom3  9350  brdom7disj  9353  brdom6disj  9354  iundom2g  9362  fpwwe2  9465  winainflem  9515  winalim2  9518  inar1  9597  tskuni  9605  nqereu  9751  prnmax  9817  genpv  9821  genpnmax  9829  genpass  9831  prlem936  9869  recexsrlem  9924  map2psrpr  9931  supsrlem  9932  axrrecex  9984  axpre-sup  9990  dedekind  10200  cnegex  10217  recex  10659  fimaxre3  10970  infm3  10982  supaddc  10990  supadd  10991  supmul1  10992  supmullem1  10993  supmullem2  10994  supmul  10995  creur  11014  creui  11015  cju  11016  nnunb  11288  arch  11289  xrsupsslem  12137  xrinfmsslem  12138  xrsupss  12139  xrinfmss  12140  xrub  12142  supxrunb1  12149  supxrunb2  12150  infmremnf  12173  infmrp1  12174  modmuladd  12712  fsequb2  12775  hashge2el2difr  13263  iswrd  13307  wrdval  13308  csbwrdg  13334  cshword  13537  0csh0  13539  2cshwcshw  13571  scshwfzeqfzo  13572  cshimadifsn  13575  shftfval  13810  abs1m  14075  rexfiuz  14087  limsupbnd2  14214  clim  14225  rlim  14226  rlim2  14227  rlim0  14239  rlim0lt  14240  ello1mpt2  14253  o1lo1  14268  o1compt  14318  rlimdiv  14376  climsup  14400  sumeq1  14419  sumeq2w  14422  summo  14448  fsum  14451  fsumcvg3  14460  infcvgaux2i  14590  mertenslem1  14616  mertenslem2  14617  mertens  14618  prodeq1f  14638  prodeq2w  14642  prodmo  14666  fprod  14671  divides  14985  odd2np1lem  15064  opeo  15089  omeo  15090  divalglem4  15119  divalglem10  15125  divalg  15126  gcdcllem3  15223  zeqzmulgcd  15232  bezoutlem1  15256  exprmfct  15416  nnnn0modprm0  15511  pythagtriplem2  15522  pythagtrip  15539  pceu  15551  pcprmpw2  15586  unbenlem  15612  4sqlem12  15660  vdwapval  15677  vdwapun  15678  vdwmc2  15683  vdwpc  15684  vdwlem2  15686  vdwlem10  15694  vdwlem13  15697  vdwnnlem1  15699  rami  15719  cshwsiun  15806  cshwrepswhash1  15809  brssc  16474  isdrs  16934  drsdir  16935  drsdirfi  16938  isdrs2  16939  ipodrsima  17165  gsumvalx  17270  gsumpropd  17272  gsumress  17276  isnsgrp  17288  sgrp2nmndlem5  17416  grpinvex  17432  dfgrp2  17447  grpidinv2  17474  grpidinv  17475  dfgrp3lem  17513  grp1  17522  imasgrp2  17530  conjnmzb  17695  gaorb  17740  orbsta  17746  symgfix2  17836  symgextfo  17842  pmtrprfvalrn  17908  psgnunilem3  17916  psgneu  17926  psgnval  17927  psgnvali  17928  psgnvalii  17929  ispgp  18007  subgpgp  18012  sylow1  18018  pgpfi  18020  sylow2blem3  18037  fislw  18040  sylow3lem2  18043  lsmelvalm  18066  lsmass  18083  pj1fval  18107  pj1val  18108  pj1eu  18109  pj1id  18112  efgrelexlema  18162  efgrelexlemb  18163  efgredeu  18165  cyggeninv  18285  cygabl  18292  pgpfac1lem2  18474  pgpfac1lem3  18476  pgpfac1lem4  18477  pgpfac1  18479  pgpfaclem2  18481  pgpfac  18483  dvdsrval  18645  dvdsr  18646  subrgdvds  18794  lss1d  18963  lspsn  19002  lspsnel  19003  lspsolvlem  19142  rspsn  19254  opsrval  19474  znf1o  19900  cygznlem3  19918  psgndiflemA  19947  ellspd  20141  mat1dimelbas  20277  mat1dimbas  20278  scmatval  20310  scmatel  20311  scmateALT  20318  mat0scmat  20344  decpmataa0  20573  decpmatmulsumfsupp  20578  pmatcollpw2lem  20582  pm2mpmhmlem1  20623  chpscmat  20647  basis2  20755  eltg2  20762  tg2  20769  isclo  20891  neival  20906  isnei  20907  isneip  20909  restbas  20962  neitr  20984  cnpval  21040  iscnp  21041  cnpimaex  21060  lmbr  21062  lmbr2  21063  cnprest2  21094  lmff  21105  regsep  21138  pnrmopn  21147  nrmsep3  21159  isnrm2  21162  iscmp  21191  cmpsublem  21202  cmpsub  21203  tgcmp  21204  sscmp  21208  hauscmplem  21209  1stcclb  21247  1stcfb  21248  is2ndc  21249  2ndc1stc  21254  1stcrest  21256  2ndcctbss  21258  1stcelcls  21264  llyeq  21273  nllyeq  21274  hausllycmp  21297  lly1stc  21299  refssex  21314  refun0  21318  islocfin  21320  locfinnei  21326  comppfsc  21335  txbas  21370  ptval  21373  ptpjopn  21415  ptclsg  21418  txcnp  21423  ptcnp  21425  txrest  21434  ptrescn  21442  txcmp  21446  tx1stc  21453  xkococn  21463  kqreglem1  21544  fbasssin  21640  fbssfi  21641  fbssint  21642  fbun  21644  fgss2  21678  fgcl  21682  ufli  21718  fmfnfmlem3  21760  fbflim2  21781  hauspwpwf1  21791  flfneii  21796  flftg  21800  txflf  21810  fclscf  21829  alexsubb  21850  alexsubALT  21855  tsmssubm  21946  ustincl  22011  ustdiag  22012  ustinvel  22013  ustexhalf  22014  ust0  22023  trust  22033  elutop  22037  ucnval  22081  ucncn  22089  cfiluexsm  22094  cfiluweak  22099  blssps  22229  blss  22230  imasf1oxms  22294  mopni  22297  metss  22313  metrest  22329  metcnp3  22345  cfilucfil  22364  metuel2  22370  nlmvscn  22491  nrginvrcn  22496  icccmplem1  22625  icccmplem2  22626  icccmp  22628  divcn  22671  cncfval  22691  elcncf2  22693  cncfmet  22711  cnheibor  22754  evth  22758  lebnumlem3  22762  lebnum  22763  xlebnum  22764  lebnumii  22765  ipcn  23045  lmmbr  23056  lmmbr2  23057  cfilfval  23062  cfili  23066  iscfil3  23071  caufval  23073  iscau  23074  iscau2  23075  equivcfil  23097  equivcau  23098  lmcau  23111  ovolval  23242  elovolm  23243  ovolgelb  23248  ovoliunlem1  23270  ovoliun2  23274  ovolshftlem1  23277  ovolscalem1  23281  ovolicc  23291  ioombl1lem4  23329  uniioombllem2  23351  mbfaddlem  23427  mbfsup  23431  mbfinf  23432  mbflimsup  23433  i1fmulc  23470  itg1climres  23481  itg2val  23495  itg2l  23496  itg2leub  23501  itg2seq  23509  itg2monolem1  23517  itg2mono  23520  itg2i1fseq2  23523  cniccibl  23607  ellimc3  23643  limciun  23658  dvferm1  23748  dvferm2  23750  lhop1lem  23776  ply1divex  23896  ig1peu  23931  plyval  23949  elply2  23952  coeval  23979  coeeu  23981  coelem  23982  coeeq  23983  plydivlem4  24051  plydivex  24052  aannenlem2  24084  aalioulem2  24088  aaliou2  24095  ulmval  24134  ulm2  24139  ulmcau  24149  ulmdvlem3  24156  abelthlem9  24194  abelth  24195  efif1olem4  24291  eflogeq  24348  efopn  24404  cxpcn3  24489  cxpeq  24498  rlimcnp  24692  lgamgulmlem6  24760  muval  24858  dchrptlem1  24989  dchrptlem2  24990  lgsdchrval  25079  2lgslem1b  25117  pntpbnd  25277  pntibndlem3  25281  pntibnd  25282  pntlemi  25293  pntleme  25297  pntlemp  25299  pnt3  25301  istrkgld  25358  istrkg3ld  25360  axtgsegcon  25363  axtgpasch  25366  axtgcont1  25367  axtgupdim2  25370  legov  25480  islnopp  25631  ishpg  25651  hpgbr  25652  hpgcom  25659  iscgra  25701  iscgra1  25702  isinag  25729  isleag  25733  ttgval  25755  ttgitvval  25762  ttgelitv  25763  brbtwn  25779  brcgr  25780  axpasch  25821  axlowdim2  25840  axlowdim  25841  axcontlem2  25845  axcontlem4  25847  axcontlem7  25850  axcontlem8  25851  upgredg2vtx  26036  edglnl  26038  usgredg4  26109  ushgredgedg  26121  ushgredgedgloop  26123  dfnbgr2  26235  nbgrel  26238  nbumgrvtx  26242  nbgrnself  26257  uvtxael1  26296  uvtxa01vtx0  26297  cusgrfilem2  26352  cusgrfi  26354  vtxd0nedgb  26384  fusgrn0degnn0  26395  wlkonl1iedg  26561  wspniunwspnon  26819  elwwlks2on  26852  clwwlksnscsh  26940  erclwwlksneq  26944  eleclclwwlksn  26953  hashecclwwlksn1  26954  umgrhashecclwwlk  26955  3cyclfrgrrn1  27149  friendshipgt3  27256  isgrpo  27351  isgrpoi  27352  grpoidinvlem3  27360  grpoideu  27363  grpoidinv2  27369  nmoofval  27617  nmooval  27618  nmosetn0  27620  nmoolb  27626  nmoubi  27627  nmlno0lem  27648  chcompl  28099  pjhthmo  28161  pjhval  28256  pjpreeq  28257  h1de2ci  28415  elspansn  28425  nmopval  28715  nmopsetn0  28724  nmfnval  28735  nmfnsetn0  28737  eigvecval  28755  hhcno  28763  hhcnf  28764  nmoplb  28766  nmopub  28767  nmfnlb  28783  nmfnleub  28784  eleigvec  28816  nmlnop0iALT  28854  nmopun  28873  nmcexi  28885  branmfn  28964  pjnmopi  29007  cvbr  29141  hatomic  29219  chrelat2  29229  cdjreui  29291  cdj3lem2  29294  reuxfr4d  29330  elabreximd  29348  br8d  29422  unipreima  29446  abfmpunirn  29452  curry2ima  29486  toslublem  29667  tosglblem  29669  archirng  29742  archiexdiv  29744  archiabllem2a  29748  archiabl  29752  isarchiofld  29817  crefi  29914  pcmplfin  29927  pstmfval  29939  tpr2rico  29958  rge0scvg  29995  ismntop  30070  esumc  30113  esumpcvgval  30140  esum2dlem  30154  inelsros  30241  diffiunisros  30242  dya2icoseg2  30340  dya2iocuni  30345  eulerpartlemgvv  30438  eulerpartlemgh  30440  hgt749d  30727  tgoldbachgt  30741  bnj66  30930  bnj873  30994  bnj18eq1  30997  bnj1234  31081  bnj1318  31093  subfacp1lem3  31164  pconncn  31206  cnpconn  31212  txpconn  31214  connpconn  31217  iscvm  31241  cvmcov  31245  cvmopnlem  31260  cvmliftlem15  31280  cvmlift3lem2  31302  cvmlift3lem4  31304  cvmlift3  31310  br8  31646  br6  31647  br4  31648  dfrdg2  31701  dfrdg3  31702  orderseqlem  31749  poseq  31750  soseq  31751  elno  31799  sltval  31800  noprefixmo  31848  nosupno  31849  nosupdm  31850  nosupfv  31852  nosupres  31853  nosupbnd1lem1  31854  nosupbnd1lem3  31856  nosupbnd1lem4  31857  nosupbnd1lem5  31858  noeta  31868  altxpeq2  32081  funtransport  32138  fvtransport  32139  brcolinear2  32165  colineardim1  32168  segcon2  32212  brsegle  32215  funray  32247  fvray  32248  funline  32249  linedegen  32250  fvline  32251  ellines  32259  gtinfOLD  32314  nn0prpwlem  32317  fnessref  32352  neibastop2lem  32355  neibastop2  32356  tailfb  32372  unblimceq0lem  32497  unblimceq0  32498  unbdqndv2  32502  bj-finsumval0  33147  relowlssretop  33211  phpreu  33393  matunitlindflem2  33406  ptrest  33408  poimirlem4  33413  poimirlem17  33426  poimirlem20  33429  poimirlem24  33433  poimirlem26  33435  poimirlem27  33436  poimirlem28  33437  poimirlem31  33440  poimirlem32  33441  poimir  33442  heicant  33444  mblfinlem1  33446  mblfinlem3  33448  mblfinlem4  33449  ismblfin  33450  itg2addnclem  33461  itg2addnclem3  33463  itg2addnc  33464  itg2gt0cn  33465  cnicciblnc  33481  ftc1anclem6  33490  unirep  33507  indexa  33528  sdclem2  33538  sdclem1  33539  sdc  33540  fdc  33541  fdc1  33542  incsequz  33544  istotbnd  33568  sstotbnd2  33573  equivtotbnd  33577  isbnd  33579  bndss  33585  ssbnd  33587  totbndbnd  33588  ismtybndlem  33605  heibor1lem  33608  heiborlem1  33610  heiborlem6  33615  heiborlem8  33617  heiborlem10  33619  heibor  33620  rngoid  33701  isgrpda  33754  isdrngo2  33757  divrngidl  33827  prnc  33866  isfldidl  33867  exanres3  34064  prtlem5  34145  prtlem13  34153  prtlem16  34154  islshp  34266  lsmsat  34295  lcvbr  34308  lsatcv0  34318  lshpsmreu  34396  lshpkrlem1  34397  lshpkrlem2  34398  lshpkrlem3  34399  lshpkrcl  34403  lshpset2N  34406  islshpkrN  34407  cvrval  34556  atlex  34603  glbconxN  34664  hlsuprexch  34667  islln  34792  islpln  34816  islpln5  34821  lvolex3N  34824  islvol  34859  islvol5  34865  ispointN  35028  pmapglbx  35055  paddval  35084  elpaddn0  35086  elpaddat  35090  elpadd0  35095  4atex  35362  4atex2  35363  cdlemefrs29bpre1  35685  cdlemefrs32fva  35688  cdlemg33b  35995  dvhb1dimN  36274  dvhopellsm  36406  dib1dim  36454  diclspsn  36483  dihglblem2aN  36582  dihglblem2N  36583  dih1dimatlem  36618  dvh3dimatN  36728  dvh2dim  36734  dvh3dim  36735  dvh4dimN  36736  dvh3dim3N  36738  dochfl1  36765  lcfl7N  36790  lcf1o  36840  lcfrlem39  36870  mapdpglem3  36964  hvmapvalvalN  37050  hdmap14lem2a  37159  hdmapglem7a  37219  elrfi  37257  isnacs  37267  nacsfg  37268  nacsfix  37275  mzpcompact2lem  37314  eldiophb  37320  eldioph  37321  eldioph2  37325  eldioph2b  37326  eldioph3  37329  eldiophss  37338  diophrex  37339  sbcrexgOLD  37349  sbc2rexgOLD  37352  rexrabdioph  37358  rexfrabdioph  37359  elnn0rabdioph  37367  dvdsrabdioph  37374  eldioph4b  37375  eldioph4i  37376  diophren  37377  rencldnfilem  37384  pell1234qrdich  37425  jm2.27  37575  expdiophlem1  37588  wepwsolem  37612  aomclem8  37631  islnr3  37685  lnr2i  37686  lpirlnr  37687  hbtlem1  37693  hbtlem2  37694  hbtlem7  37695  hbtlem4  37696  hbtlem5  37698  hbtlem6  37699  dgraaval  37714  dgraalem  37715  dgraaub  37718  rngunsnply  37743  brtrclfv2  38019  clsk1indlem1  38343  extoimad  38464  elabrexg  39206  foelrnf  39373  disjrnmpt2  39375  upbdrech  39519  ssfiunibd  39523  supxrgere  39549  supxrgelem  39553  supxrge  39554  suplesup  39555  infxr  39583  infleinf  39588  supxrunb3  39623  unb2ltle  39642  uzub  39658  supminfxr  39694  iccshift  39744  iooshift  39748  climinf  39838  climinff  39843  ellimcabssub0  39849  climf  39854  limcperiod  39860  limclner  39883  climf2  39898  clim2d  39905  limsupref  39917  limsuppnfd  39934  limsuppnf  39943  climinfmpt  39947  limsupubuzmpt  39951  limsupmnf  39953  limsupre2lem  39956  limsupre2  39957  limsupmnfuz  39959  limsupre2mpt  39962  limsupre3lem  39964  limsupre3  39965  limsupre3mpt  39966  limsupre3uzlem  39967  limsupre3uz  39968  limsupreuz  39969  limsupreuzmpt  39971  climuz  39976  liminfreuzlem  40034  liminfreuz  40035  xlimmnfvlem1  40058  xlimmnfv  40060  xlimpnfvlem1  40062  xlimpnfv  40064  cncfshiftioo  40105  fperdvper  40133  itgiccshift  40196  itgperiod  40197  stoweidlem27  40244  stoweidlem31  40248  stoweidlem43  40260  stoweidlem46  40263  stoweidlem52  40269  stoweidlem60  40277  fourierdlem42  40366  fourierdlem48  40371  fourierdlem51  40374  fourierdlem54  40377  fourierdlem63  40386  fourierdlem64  40387  fourierdlem65  40388  fourierdlem68  40391  fourierdlem70  40393  fourierdlem71  40394  fourierdlem73  40396  fourierdlem80  40403  fourierdlem81  40404  fourierdlem89  40412  fourierdlem90  40413  fourierdlem91  40414  fourierdlem92  40415  fourierdlem96  40419  fourierdlem97  40420  fourierdlem98  40421  fourierdlem99  40422  fourierdlem100  40423  fourierdlem103  40426  fourierdlem104  40427  fourierdlem105  40428  fourierdlem108  40431  fourierdlem109  40432  fourierdlem110  40433  fourierdlem112  40435  fourierdlem113  40436  sge0pnffigt  40613  sge0resplit  40623  ovnval2  40759  ovnval2b  40766  ovnlecvr  40772  ovnpnfelsup  40773  ovn0lem  40779  ovnsubaddlem1  40784  hoidmvlelem1  40809  ovnhoilem1  40815  ovnhoi  40817  ovnlecvr2  40824  hoiqssbl  40839  ovolval5lem2  40867  ovolval5lem3  40868  ovolval5  40869  ovnovol  40873  smfsuplem2  41018  smfsup  41020  smfinflem  41023  smfinf  41024  cbvrex2  41173  afvelrnb  41243  afvelrnb0  41244  iccelpart  41369  iccpartiun  41370  icceuelpart  41372  cshword2  41437  fmtnofac2lem  41480  fmtnofac2  41481  fmtnofac1  41482  m1expevenALTV  41560  odd2np1ALTV  41585  opoeALTV  41594  opeoALTV  41595  mogoldbblem  41629  isgbow  41640  isgbo  41641  7gbow  41660  9gbo  41662  11gbo  41663  sbgoldbwt  41665  mogoldbb  41673  sbgoldbo  41675  nnsum3primesgbe  41680  nnsum4primesodd  41684  nnsum4primesoddALTV  41685  bgoldbtbnd  41697  sprsymrelf1lem  41741  sprsymrelf  41745  uspgrsprf1  41755  uspgrsprfo  41756  0nodd  41810  1odd  41811  2nodd  41812  0even  41931  1neven  41932  2even  41933  2zlidl  41934  2zrngamgm  41939  2zrngagrp  41943  2zrngmmgm  41946  2zrngnmrid  41950  lcoval  42201  el0ldep  42255  ldepspr  42262  zlmodzxzldep  42293