MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  rexbidv Unicode version

Theorem rexbidv 2695
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
StepHypRef Expression
1 nfv 1626 . 2  |-  F/ x ph
2 ralbidv.1 . 2  |-  ( ph  ->  ( ps  <->  ch )
)
31, 2rexbid 2693 1  |-  ( ph  ->  ( E. x  e.  A  ps  <->  E. x  e.  A  ch )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177   E.wrex 2675
This theorem is referenced by:  rexbii  2699  2rexbidv  2717  rexralbidv  2718  rexeqbi1dv  2881  rexeqbidv  2885  cbvrex2v  2909  rspc2ev  3028  rspc3ev  3030  ceqsrex2v  3039  sbcrexg  3204  uniiunlem  3399  eliun  4065  dfiin2g  4092  dfiunv2  4095  orduninsuc  4790  elrnmpt  5084  elrnmptg  5087  elimag  5174  funcnvuni  5485  fun11iun  5662  fvelrnb  5741  fvelimab  5749  foelrn  5855  foco2  5856  elabrex  5952  abrexco  5953  abrexex2g  5955  abrexex2  5968  f1oiso  6038  f1oiso2  6039  f1oweALT  6041  grprinvlem  6252  recseq  6601  tfrlem3  6605  tfrlem3a  6606  tfrlem12  6617  seqomlem2  6675  nneob  6862  qseq2  6922  elqsg  6923  elixpsn  7068  ixpsnf1o  7069  isfi  7098  enfi  7292  pssnn  7294  frfi  7319  unblem1  7326  unblem2  7327  unbnn2  7331  fofinf1o  7354  finsschain  7379  indexfi  7380  elfi  7384  marypha1lem  7404  supmo  7421  suplub  7429  supisolem  7439  oieq1  7445  ordtypelem2  7452  ordtypelem3  7453  ordtypelem9  7459  wemaplem1  7479  brwdom2  7505  brwdom3  7514  unwdomg  7516  oemapval  7603  cantnf  7613  wemapwe  7618  cnfcom3clem  7626  tz9.13  7681  tz9.13g  7682  cardf2  7794  isnum2  7796  ennum  7798  cardiun  7833  infxpenc2  7867  aceq1  7962  aceq2  7964  dfac5lem3  7970  dfac5lem4  7971  dfac2a  7974  dfac2  7975  kmlem9  8002  kmlem12  8005  kmlem14  8007  ackbij1  8082  cflm  8094  cfss  8109  cofsmo  8113  cfsmolem  8114  cfcoflem  8116  coftr  8117  isfin7  8145  fin23lem26  8169  isf32lem5  8201  fin1a2lem11  8254  hsmexlem2  8271  axdc3lem3  8296  axdc3  8298  numthcor  8338  zorn2lem7  8346  brdom3  8370  brdom7disj  8373  brdom6disj  8374  iundom2g  8379  fpwwe2  8482  winainflem  8532  winalim2  8535  inar1  8614  tskuni  8622  nqereu  8770  prnmax  8836  genpv  8840  genpnmax  8848  genpass  8850  prlem936  8888  recexsrlem  8942  map2psrpr  8949  supsrlem  8950  axrrecex  9002  axpre-sup  9008  cnegex  9211  recex  9618  fimaxre3  9921  infm3  9931  supmul1  9937  supmullem1  9938  supmullem2  9939  supmul  9940  creur  9958  creui  9959  cju  9960  nnunb  10181  arch  10182  xrsupsslem  10849  xrinfmsslem  10850  xrsupss  10851  xrinfmss  10852  xrub  10854  supxrunb1  10862  supxrunb2  10863  infmxrgelb  10877  fsequb2  11278  iswrd  11692  wrdval  11693  shftfval  11848  abs1m  12102  rexfiuz  12114  limsupbnd2  12240  clim  12251  rlim  12252  rlim2  12253  rlim0  12265  rlim0lt  12266  ello1mpt2  12279  o1lo1  12294  o1compt  12344  rlimdiv  12402  climsup  12426  sumeq1f  12445  sumeq2w  12449  cbvsum  12452  summo  12474  fsum  12477  fsumcvg3  12486  infcvgaux2i  12600  mertenslem1  12624  mertenslem2  12625  mertens  12626  divides  12817  odd2np1lem  12870  divalglem4  12879  divalglem10  12885  divalg  12886  gcdcllem3  12976  bezoutlem1  13001  exprmfct  13073  opeo  13150  omeo  13151  pythagtriplem2  13154  pythagtrip  13171  pceu  13183  pcprmpw2  13218  unbenlem  13239  4sqlem12  13287  vdwapval  13304  vdwapun  13305  vdwmc2  13310  vdwpc  13311  vdwlem2  13313  vdwlem10  13321  vdwlem13  13324  vdwnnlem1  13326  rami  13346  brssc  13977  isdrs  14354  drsdir  14355  drsdirfi  14358  isdrs2  14359  ipodrsima  14554  spwpr4  14626  gsumvalx  14737  gsumpropd  14739  gsumress  14740  grpinvex  14783  imasgrp2  14896  conjnmzb  15003  gaorb  15047  orbsta  15053  ispgp  15189  subgpgp  15194  sylow1  15200  pgpfi  15202  sylow2blem3  15219  fislw  15222  sylow3lem2  15225  lsmelvalm  15248  lsmass  15265  pj1fval  15289  pj1val  15290  pj1eu  15291  pj1id  15294  efgrelexlema  15344  efgrelexlemb  15345  efgredeu  15347  cyggeninv  15456  cygabl  15463  pgpfac1lem2  15596  pgpfac1lem3  15598  pgpfac1lem4  15599  pgpfac1  15601  pgpfaclem2  15603  pgpfac  15605  dvdsrval  15713  dvdsr  15714  subrgdvds  15845  lss1d  16002  lspsn  16041  lspsnel  16042  lspsolvlem  16177  rspsn  16288  opsrval  16498  znf1o  16795  cygznlem3  16813  basis2  16979  eltg2  16986  tg2  16993  isclo  17114  neival  17129  isnei  17130  isneip  17132  restbas  17184  neitr  17206  cnpval  17262  iscnp  17263  cnpimaex  17282  lmbr  17284  lmbr2  17285  cnprest2  17316  lmff  17327  regsep  17360  pnrmopn  17369  nrmsep3  17381  isnrm2  17384  iscmp  17413  cmpsublem  17424  cmpsub  17425  tgcmp  17426  sscmp  17430  hauscmplem  17431  1stcclb  17468  1stcfb  17469  is2ndc  17470  2ndc1stc  17475  1stcrest  17477  2ndcctbss  17479  1stcelcls  17485  llyeq  17494  nllyeq  17495  hausllycmp  17518  lly1stc  17520  txbas  17560  ptval  17563  ptpjopn  17605  ptclsg  17608  txcnp  17613  ptcnp  17615  txrest  17624  ptrescn  17632  txcmp  17636  tx1stc  17643  xkococn  17653  kqreglem1  17734  fbasssin  17829  fbssfi  17830  fbssint  17831  fbun  17833  fgss2  17867  fgcl  17871  ufli  17907  fmfnfmlem3  17949  fbflim2  17970  hauspwpwf1  17980  flfneii  17985  flftg  17989  txflf  17999  fclscf  18018  alexsubb  18038  alexsubALT  18043  tsmssubm  18133  ustincl  18198  ustdiag  18199  ustinvel  18200  ustexhalf  18201  ust0  18210  trust  18220  elutop  18224  ucnval  18268  ucncn  18276  cfiluexsm  18281  cfiluweak  18286  blssps  18415  blss  18416  imasf1oxms  18480  mopni  18483  metss  18499  metrest  18515  metcnp3  18531  cfilucfilOLD  18560  cfilucfil  18561  metuel2  18570  nlmvscn  18684  nrginvrcn  18688  icccmplem1  18814  icccmplem2  18815  icccmp  18817  divcn  18859  cncfval  18879  elcncf2  18881  cncfmet  18899  cnheibor  18941  evth  18945  lebnumlem3  18949  lebnum  18950  xlebnum  18951  lebnumii  18952  ipcn  19161  lmmbr  19172  lmmbr2  19173  cfilfval  19178  cfili  19182  iscfil3  19187  caufval  19189  iscau  19190  iscau2  19191  equivcfil  19213  equivcau  19214  lmcau  19226  ovolval  19331  elovolm  19332  ovolgelb  19337  ovoliunlem1  19359  ovoliun2  19363  ovolshftlem1  19366  ovolscalem1  19370  ovolicc  19380  ioombl1lem4  19416  uniioombllem2  19436  mbfaddlem  19513  mbfsup  19517  mbfinf  19518  mbflimsup  19519  i1fmulc  19556  itg1climres  19567  itg2val  19581  itg2l  19582  itg2leub  19587  itg2seq  19595  itg2monolem1  19603  itg2mono  19606  itg2i1fseq2  19609  cniccibl  19693  ellimc3  19727  limciun  19742  dvferm1  19830  dvferm2  19832  lhop1lem  19858  ply1divex  20020  ig1peu  20055  plyval  20073  elply2  20076  coeval  20103  coeeu  20105  coelem  20106  coeeq  20107  plydivlem4  20174  plydivex  20175  aannenlem2  20207  aalioulem2  20211  aaliou2  20218  ulmval  20257  ulm2  20262  ulmcau  20272  ulmdvlem3  20279  abelthlem9  20317  abelth  20318  efif1olem4  20408  eflogeq  20457  efopn  20510  cxpcn3  20593  cxpeq  20602  rlimcnp  20765  muval  20876  dchrptlem1  21009  dchrptlem2  21010  lgsdchrval  21092  pntpbnd  21243  pntibndlem3  21247  pntibnd  21248  pntlemi  21259  pntleme  21263  pntlemp  21265  pnt3  21267  nbgraf1olem1  21412  cusgrafilem2  21450  cusgrafi  21452  iseupa  21648  isgrpo  21745  isgrpoi  21747  grpoidinvlem3  21755  grpoideu  21758  grpoidinv2  21767  isgrp2d  21784  isgrpda  21846  ghgrp  21917  rngoid  21932  nmoofval  22224  nmooval  22225  nmosetn0  22227  nmoolb  22233  nmoubi  22234  nmlno0lem  22255  chcompl  22706  pjhthmo  22765  pjhval  22860  pjpreeq  22861  h1de2ci  23019  elspansn  23029  nmopval  23320  nmopsetn0  23329  nmfnval  23340  nmfnsetn0  23342  eigvecval  23360  hhcno  23368  hhcnf  23369  nmoplb  23371  nmopub  23372  nmfnlb  23388  nmfnleub  23389  eleigvec  23421  nmlnop0iALT  23459  nmopun  23478  nmcexi  23490  branmfn  23569  pjnmopi  23612  cvbr  23746  hatomic  23824  chrelat2  23834  cdjreui  23896  cdj3lem2  23899  reuxfr4d  23938  elabreximd  23952  unipreima  24017  abfmpunirn  24025  curry2ima  24058  toslub  24152  tosglb  24153  pstmfval  24252  tpr2rico  24271  rge0scvg  24296  esumc  24407  esumpcvgval  24429  dya2icoseg2  24589  dya2iocuni  24594  lgamgulmlem6  24779  subfacp1lem3  24829  pconcn  24872  cnpcon  24878  txpcon  24880  conpcon  24883  iscvm  24907  cvmcov  24911  cvmopnlem  24926  cvmliftlem15  24946  cvmlift3lem2  24968  cvmlift3lem4  24970  cvmlift3  24976  dedekind  25148  prodeq1f  25195  prodeq2w  25199  prodmo  25223  fprod  25228  br8  25335  br6  25336  br4  25337  dfrdg2  25374  dfrdg3  25375  orderseqlem  25474  poseq  25475  soseq  25476  elno  25522  sltval  25523  nobndlem6  25573  nofulllem1  25578  nofulllem2  25579  nofulllem5  25582  altxpeq2  25731  brbtwn  25750  brcgr  25751  axpasch  25792  axlowdim2  25811  axlowdim  25812  axcontlem2  25816  axcontlem4  25818  axcontlem7  25821  axcontlem8  25822  funtransport  25877  fvtransport  25878  brcolinear2  25904  colineardim1  25907  segcon2  25951  brsegle  25954  funray  25986  fvray  25987  funline  25988  linedegen  25989  fvline  25990  ellines  25998  supaddc  26145  supadd  26146  mblfinlem  26151  mblfinlem2  26152  mblfinlem3  26153  ismblfin  26154  itg2addnclem  26163  itg2addnclem3  26165  itg2addnc  26166  itg2gt0cn  26167  cnicciblnc  26183  gtinf  26220  nn0prpwlem  26223  refssex  26259  fnessref  26271  islocfin  26274  locfinnei  26280  comppfsc  26285  neibastop2lem  26287  neibastop2  26288  tailfb  26304  unirep  26312  indexa  26333  sdclem2  26344  sdclem1  26345  sdc  26346  fdc  26347  fdc1  26348  incsequz  26350  istotbnd  26376  sstotbnd2  26381  equivtotbnd  26385  isbnd  26387  bndss  26393  ssbnd  26395  totbndbnd  26396  ismtybndlem  26413  heibor1lem  26416  heiborlem1  26418  heiborlem6  26423  heiborlem8  26425  heiborlem10  26427  heibor  26428  isdrngo2  26472  divrngidl  26536  prnc  26575  isfldidl  26576  prtlem5  26603  prtlem13  26615  prtlem16  26616  elrfi  26646  isnacs  26656  nacsfg  26657  nacsfix  26664  mzpcompact2lem  26706  eldiophb  26713  eldioph  26714  eldioph2  26718  eldioph2b  26719  eldioph3  26722  eldiophss  26731  diophrex  26732  sbc2rexg  26742  rexrabdioph  26752  rexfrabdioph  26753  elnn0rabdioph  26761  dvdsrabdioph  26768  eldioph4b  26770  eldioph4i  26771  diophren  26772  rencldnfilem  26779  pell1234qrdich  26822  jm2.27  26977  expdiophlem1  26990  wepwsolem  27014  aomclem8  27035  ellspd  27130  islnr3  27195  lnr2i  27196  lpirlnr  27197  hbtlem1  27203  hbtlem2  27204  hbtlem7  27205  hbtlem4  27206  hbtlem5  27208  hbtlem6  27209  dgraaval  27225  dgraalem  27226  dgraaub  27229  rngunsnply  27254  psgnunilem3  27295  psgneu  27305  psgnval  27306  psgnvali  27307  psgnvalii  27308  infrglb  27597  climinf  27607  climinff  27612  stoweidlem27  27651  stoweidlem31  27655  stoweidlem43  27667  stoweidlem46  27670  stoweidlem52  27676  stoweidlem60  27684  cbvrex2  27826  afvelrnb  27902  afvelrnb0  27903  el2xptp  27956  el2wlksot  28085  el2pthsot  28086  2wot2wont  28091  2spot2iun2spont  28096  frgra2v  28111  3cyclfrgrarn1  28124  frgrancvvdeqlem4  28144  bnj66  28949  bnj873  29013  bnj18eq1  29016  bnj1234  29100  bnj1318  29112  islshp  29474  lsmsat  29503  lcvbr  29516  lsatcv0  29526  lshpsmreu  29604  lshpkrlem1  29605  lshpkrlem2  29606  lshpkrlem3  29607  lshpkrcl  29611  lshpset2N  29614  islshpkrN  29615  cvrval  29764  atlex  29811  glbconxN  29872  hlsuprexch  29875  islln  30000  islpln  30024  islpln5  30029  lvolex3N  30032  islvol  30067  islvol5  30073  ispointN  30236  pmapglbx  30263  paddval  30292  elpaddn0  30294  elpaddat  30298  elpadd0  30303  4atex  30570  4atex2  30571  cdlemefrs29bpre1  30891  cdlemefrs32fva  30894  cdlemg33b  31201  dvhb1dimN  31480  dvhopellsm  31612  dib1dim  31660  diclspsn  31689  dihglblem2aN  31788  dihglblem2N  31789  dih1dimatlem  31824  dvh3dimatN  31934  dvh2dim  31940  dvh3dim  31941  dvh4dimN  31942  dvh3dim3N  31944  dochfl1  31971  lcfl7N  31996  lcf1o  32046  lcfrlem39  32076  mapdpglem3  32170  hvmapvalvalN  32256  hdmap14lem2a  32365  hdmapglem7a  32425
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 2680
  Copyright terms: Public domain W3C validator