Theorem rexbidv 2687

Description: Formula-building rule for restricted existential quantifier (deduction rule). (Contributed by NM, 20-Nov-1994.)

Hypothesis

Ref	Expression
ralbidv.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		nfv 1626	. 2 |- F/ x ph
2		ralbidv.1	. 2 |- ( ph -> ( ps <-> ch ) )
3	1, 2	rexbid 2685	1 |- ( ph -> ( E. x e. A ps <-> E. x e. A ch ) )

Syntax hints:   -> wi 4   <-> wb 177   E.wrex 2667

This theorem is referenced by:  rexbii  2691  2rexbidv  2709  rexralbidv  2710  rexeqbi1dv  2873  rexeqbidv  2877  cbvrex2v  2901  rspc2ev  3020  rspc3ev  3022  ceqsrex2v  3031  sbcrexg  3196  uniiunlem  3391  eliun  4057  dfiin2g  4084  dfiunv2  4087  orduninsuc  4782  elrnmpt  5076  elrnmptg  5079  elimag  5166  funcnvuni  5477  fun11iun  5654  fvelrnb  5733  fvelimab  5741  foelrn  5847  foco2  5848  elabrex  5944  abrexco  5945  abrexex2g  5947  abrexex2  5960  f1oiso  6030  f1oiso2  6031  f1oweALT  6033  grprinvlem  6244  recseq  6593  tfrlem3  6597  tfrlem3a  6598  tfrlem12  6609  seqomlem2  6667  nneob  6854  qseq2  6914  elqsg  6915  elixpsn  7060  ixpsnf1o  7061  isfi  7090  enfi  7284  pssnn  7286  frfi  7311  unblem1  7318  unblem2  7319  unbnn2  7323  fofinf1o  7346  finsschain  7371  indexfi  7372  elfi  7376  marypha1lem  7396  supmo  7413  suplub  7421  supisolem  7431  oieq1  7437  ordtypelem2  7444  ordtypelem3  7445  ordtypelem9  7451  wemaplem1  7471  brwdom2  7497  brwdom3  7506  unwdomg  7508  oemapval  7595  cantnf  7605  wemapwe  7610  cnfcom3clem  7618  tz9.13  7673  tz9.13g  7674  cardf2  7786  isnum2  7788  ennum  7790  cardiun  7825  infxpenc2  7859  aceq1  7954  aceq2  7956  dfac5lem3  7962  dfac5lem4  7963  dfac2a  7966  dfac2  7967  kmlem9  7994  kmlem12  7997  kmlem14  7999  ackbij1  8074  cflm  8086  cfss  8101  cofsmo  8105  cfsmolem  8106  cfcoflem  8108  coftr  8109  isfin7  8137  fin23lem26  8161  isf32lem5  8193  fin1a2lem11  8246  hsmexlem2  8263  axdc3lem3  8288  axdc3  8290  numthcor  8330  zorn2lem7  8338  brdom3  8362  brdom7disj  8365  brdom6disj  8366  iundom2g  8371  fpwwe2  8474  winainflem  8524  winalim2  8527  inar1  8606  tskuni  8614  nqereu  8762  prnmax  8828  genpv  8832  genpnmax  8840  genpass  8842  prlem936  8880  recexsrlem  8934  map2psrpr  8941  supsrlem  8942  axrrecex  8994  axpre-sup  9000  cnegex  9203  recex  9610  fimaxre3  9913  infm3  9923  supmul1  9929  supmullem1  9930  supmullem2  9931  supmul  9932  creur  9950  creui  9951  cju  9952  nnunb  10173  arch  10174  xrsupsslem  10841  xrinfmsslem  10842  xrsupss  10843  xrinfmss  10844  xrub  10846  supxrunb1  10854  supxrunb2  10855  infmxrgelb  10869  fsequb2  11270  iswrd  11684  wrdval  11685  shftfval  11840  abs1m  12094  rexfiuz  12106  limsupbnd2  12232  clim  12243  rlim  12244  rlim2  12245  rlim0  12257  rlim0lt  12258  ello1mpt2  12271  o1lo1  12286  o1compt  12336  rlimdiv  12394  climsup  12418  sumeq1f  12437  sumeq2w  12441  cbvsum  12444  summo  12466  fsum  12469  fsumcvg3  12478  infcvgaux2i  12592  mertenslem1  12616  mertenslem2  12617  mertens  12618  divides  12809  odd2np1lem  12862  divalglem4  12871  divalglem10  12877  divalg  12878  gcdcllem3  12968  bezoutlem1  12993  exprmfct  13065  opeo  13142  omeo  13143  pythagtriplem2  13146  pythagtrip  13163  pceu  13175  pcprmpw2  13210  unbenlem  13231  4sqlem12  13279  vdwapval  13296  vdwapun  13297  vdwmc2  13302  vdwpc  13303  vdwlem2  13305  vdwlem10  13313  vdwlem13  13316  vdwnnlem1  13318  rami  13338  brssc  13969  isdrs  14346  drsdir  14347  drsdirfi  14350  isdrs2  14351  ipodrsima  14546  spwpr4  14618  gsumvalx  14729  gsumpropd  14731  gsumress  14732  grpinvex  14775  imasgrp2  14888  conjnmzb  14995  gaorb  15039  orbsta  15045  ispgp  15181  subgpgp  15186  sylow1  15192  pgpfi  15194  sylow2blem3  15211  fislw  15214  sylow3lem2  15217  lsmelvalm  15240  lsmass  15257  pj1fval  15281  pj1val  15282  pj1eu  15283  pj1id  15286  efgrelexlema  15336  efgrelexlemb  15337  efgredeu  15339  cyggeninv  15448  cygabl  15455  pgpfac1lem2  15588  pgpfac1lem3  15590  pgpfac1lem4  15591  pgpfac1  15593  pgpfaclem2  15595  pgpfac  15597  dvdsrval  15705  dvdsr  15706  subrgdvds  15837  lss1d  15994  lspsn  16033  lspsnel  16034  lspsolvlem  16169  rspsn  16280  opsrval  16490  znf1o  16787  cygznlem3  16805  basis2  16971  eltg2  16978  tg2  16985  isclo  17106  neival  17121  isnei  17122  isneip  17124  restbas  17176  neitr  17198  cnpval  17254  iscnp  17255  cnpimaex  17274  lmbr  17276  lmbr2  17277  cnprest2  17308  lmff  17319  regsep  17352  pnrmopn  17361  nrmsep3  17373  isnrm2  17376  iscmp  17405  cmpsublem  17416  cmpsub  17417  tgcmp  17418  sscmp  17422  hauscmplem  17423  1stcclb  17460  1stcfb  17461  is2ndc  17462  2ndc1stc  17467  1stcrest  17469  2ndcctbss  17471  1stcelcls  17477  llyeq  17486  nllyeq  17487  hausllycmp  17510  lly1stc  17512  txbas  17552  ptval  17555  ptpjopn  17597  ptclsg  17600  txcnp  17605  ptcnp  17607  txrest  17616  ptrescn  17624  txcmp  17628  tx1stc  17635  xkococn  17645  kqreglem1  17726  fbasssin  17821  fbssfi  17822  fbssint  17823  fbun  17825  fgss2  17859  fgcl  17863  ufli  17899  fmfnfmlem3  17941  fbflim2  17962  hauspwpwf1  17972  flfneii  17977  flftg  17981  txflf  17991  fclscf  18010  alexsubb  18030  alexsubALT  18035  tsmssubm  18125  ustincl  18190  ustdiag  18191  ustinvel  18192  ustexhalf  18193  ust0  18202  trust  18212  elutop  18216  ucnval  18260  ucncn  18268  cfiluexsm  18273  cfiluweak  18278  blssps  18407  blss  18408  imasf1oxms  18472  mopni  18475  metss  18491  metrest  18507  metcnp3  18523  cfilucfilOLD  18552  cfilucfil  18553  metuel2  18562  nlmvscn  18676  nrginvrcn  18680  icccmplem1  18806  icccmplem2  18807  icccmp  18809  divcn  18851  cncfval  18871  elcncf2  18873  cncfmet  18891  cnheibor  18933  evth  18937  lebnumlem3  18941  lebnum  18942  xlebnum  18943  lebnumii  18944  ipcn  19153  lmmbr  19164  lmmbr2  19165  cfilfval  19170  cfili  19174  iscfil3  19179  caufval  19181  iscau  19182  iscau2  19183  equivcfil  19205  equivcau  19206  lmcau  19218  ovolval  19323  elovolm  19324  ovolgelb  19329  ovoliunlem1  19351  ovoliun2  19355  ovolshftlem1  19358  ovolscalem1  19362  ovolicc  19372  ioombl1lem4  19408  uniioombllem2  19428  mbfaddlem  19505  mbfsup  19509  mbfinf  19510  mbflimsup  19511  i1fmulc  19548  itg1climres  19559  itg2val  19573  itg2l  19574  itg2leub  19579  itg2seq  19587  itg2monolem1  19595  itg2mono  19598  itg2i1fseq2  19601  cniccibl  19685  ellimc3  19719  limciun  19734  dvferm1  19822  dvferm2  19824  lhop1lem  19850  ply1divex  20012  ig1peu  20047  plyval  20065  elply2  20068  coeval  20095  coeeu  20097  coelem  20098  coeeq  20099  plydivlem4  20166  plydivex  20167  aannenlem2  20199  aalioulem2  20203  aaliou2  20210  ulmval  20249  ulm2  20254  ulmcau  20264  ulmdvlem3  20271  abelthlem9  20309  abelth  20310  efif1olem4  20400  eflogeq  20449  efopn  20502  cxpcn3  20585  cxpeq  20594  rlimcnp  20757  muval  20868  dchrptlem1  21001  dchrptlem2  21002  lgsdchrval  21084  pntpbnd  21235  pntibndlem3  21239  pntibnd  21240  pntlemi  21251  pntleme  21255  pntlemp  21257  pnt3  21259  nbgraf1olem1  21404  cusgrafilem2  21442  cusgrafi  21444  iseupa  21640  isgrpo  21737  isgrpoi  21739  grpoidinvlem3  21747  grpoideu  21750  grpoidinv2  21759  isgrp2d  21776  isgrpda  21838  ghgrp  21909  rngoid  21924  nmoofval  22216  nmooval  22217  nmosetn0  22219  nmoolb  22225  nmoubi  22226  nmlno0lem  22247  chcompl  22698  pjhthmo  22757  pjhval  22852  pjpreeq  22853  h1de2ci  23011  elspansn  23021  nmopval  23312  nmopsetn0  23321  nmfnval  23332  nmfnsetn0  23334  eigvecval  23352  hhcno  23360  hhcnf  23361  nmoplb  23363  nmopub  23364  nmfnlb  23380  nmfnleub  23381  eleigvec  23413  nmlnop0iALT  23451  nmopun  23470  nmcexi  23482  branmfn  23561  pjnmopi  23604  cvbr  23738  hatomic  23816  chrelat2  23826  cdjreui  23888  cdj3lem2  23891  reuxfr4d  23930  elabreximd  23944  unipreima  24009  abfmpunirn  24017  curry2ima  24050  toslub  24144  tosglb  24145  pstmfval  24244  tpr2rico  24263  rge0scvg  24288  esumc  24399  esumpcvgval  24421  dya2icoseg2  24581  dya2iocuni  24586  lgamgulmlem6  24771  subfacp1lem3  24821  pconcn  24864  cnpcon  24870  txpcon  24872  conpcon  24875  iscvm  24899  cvmcov  24903  cvmopnlem  24918  cvmliftlem15  24938  cvmlift3lem2  24960  cvmlift3lem4  24962  cvmlift3  24968  dedekind  25140  prodeq1f  25187  prodeq2w  25191  prodmo  25215  fprod  25220  br8  25327  br6  25328  br4  25329  dfrdg2  25366  dfrdg3  25367  orderseqlem  25466  poseq  25467  soseq  25468  elno  25514  sltval  25515  nobndlem6  25565  nofulllem1  25570  nofulllem2  25571  nofulllem5  25574  altxpeq2  25723  brbtwn  25742  brcgr  25743  axpasch  25784  axlowdim2  25803  axlowdim  25804  axcontlem2  25808  axcontlem4  25810  axcontlem7  25813  axcontlem8  25814  funtransport  25869  fvtransport  25870  brcolinear2  25896  colineardim1  25899  segcon2  25943  brsegle  25946  funray  25978  fvray  25979  funline  25980  linedegen  25981  fvline  25982  ellines  25990  supaddc  26137  supadd  26138  mblfinlem  26143  mblfinlem2  26144  mblfinlem3  26145  ismblfin  26146  itg2addnclem  26155  itg2addnclem3  26157  itg2addnc  26158  itg2gt0cn  26159  cnicciblnc  26175  gtinf  26212  nn0prpwlem  26215  refssex  26251  fnessref  26263  islocfin  26266  locfinnei  26272  comppfsc  26277  neibastop2lem  26279  neibastop2  26280  tailfb  26296  unirep  26304  indexa  26325  sdclem2  26336  sdclem1  26337  sdc  26338  fdc  26339  fdc1  26340  incsequz  26342  istotbnd  26368  sstotbnd2  26373  equivtotbnd  26377  isbnd  26379  bndss  26385  ssbnd  26387  totbndbnd  26388  ismtybndlem  26405  heibor1lem  26408  heiborlem1  26410  heiborlem6  26415  heiborlem8  26417  heiborlem10  26419  heibor  26420  isdrngo2  26464  divrngidl  26528  prnc  26567  isfldidl  26568  prtlem5  26595  prtlem13  26607  prtlem16  26608  elrfi  26638  isnacs  26648  nacsfg  26649  nacsfix  26656  mzpcompact2lem  26698  eldiophb  26705  eldioph  26706  eldioph2  26710  eldioph2b  26711  eldioph3  26714  eldiophss  26723  diophrex  26724  sbc2rexg  26734  rexrabdioph  26744  rexfrabdioph  26745  elnn0rabdioph  26753  dvdsrabdioph  26760  eldioph4b  26762  eldioph4i  26763  diophren  26764  rencldnfilem  26771  pell1234qrdich  26814  jm2.27  26969  expdiophlem1  26982  wepwsolem  27006  aomclem8  27027  ellspd  27122  islnr3  27187  lnr2i  27188  lpirlnr  27189  hbtlem1  27195  hbtlem2  27196  hbtlem7  27197  hbtlem4  27198  hbtlem5  27200  hbtlem6  27201  dgraaval  27217  dgraalem  27218  dgraaub  27221  rngunsnply  27246  psgnunilem3  27287  psgneu  27297  psgnval  27298  psgnvali  27299  psgnvalii  27300  infrglb  27589  climinf  27599  climinff  27604  stoweidlem27  27643  stoweidlem31  27647  stoweidlem43  27659  stoweidlem46  27662  stoweidlem52  27668  stoweidlem60  27676  cbvrex2  27818  afvelrnb  27894  afvelrnb0  27895  el2xptp  27948  el2wlksot  28077  el2pthsot  28078  2wot2wont  28083  2spot2iun2spont  28088  frgra2v  28103  3cyclfrgrarn1  28116  frgrancvvdeqlem4  28136  bnj66  28937  bnj873  29001  bnj18eq1  29004  bnj1234  29088  bnj1318  29100  islshp  29462  lsmsat  29491  lcvbr  29504  lsatcv0  29514  lshpsmreu  29592  lshpkrlem1  29593  lshpkrlem2  29594  lshpkrlem3  29595  lshpkrcl  29599  lshpset2N  29602  islshpkrN  29603  cvrval  29752  atlex  29799  glbconxN  29860  hlsuprexch  29863  islln  29988  islpln  30012  islpln5  30017  lvolex3N  30020  islvol  30055  islvol5  30061  ispointN  30224  pmapglbx  30251  paddval  30280  elpaddn0  30282  elpaddat  30286  elpadd0  30291  4atex  30558  4atex2  30559  cdlemefrs29bpre1  30879  cdlemefrs32fva  30882  cdlemg33b  31189  dvhb1dimN  31468  dvhopellsm  31600  dib1dim  31648  diclspsn  31677  dihglblem2aN  31776  dihglblem2N  31777  dih1dimatlem  31812  dvh3dimatN  31922  dvh2dim  31928  dvh3dim  31929  dvh4dimN  31930  dvh3dim3N  31932  dochfl1  31959  lcfl7N  31984  lcf1o  32034  lcfrlem39  32064  mapdpglem3  32158  hvmapvalvalN  32244  hdmap14lem2a  32353  hdmapglem7a  32413

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-11 1757

This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1548  df-nf 1551  df-rex 2672