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

Theorem rexbidv 2726
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 1629 . 2  |-  F/ x ph
2 ralbidv.1 . 2  |-  ( ph  ->  ( ps  <->  ch )
)
31, 2rexbid 2724 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 2706
This theorem is referenced by:  rexbii  2730  2rexbidv  2748  rexralbidv  2749  rexeqbi1dv  2913  rexeqbidv  2917  cbvrex2v  2941  rspc2ev  3060  rspc3ev  3062  ceqsrex2v  3071  sbcrexg  3236  uniiunlem  3431  eliun  4097  dfiin2g  4124  dfiunv2  4127  orduninsuc  4823  elrnmpt  5117  elrnmptg  5120  elimag  5207  funcnvuni  5518  fun11iun  5695  fvelrnb  5774  fvelimab  5782  foelrn  5888  foco2  5889  elabrex  5985  abrexco  5986  abrexex2g  5988  abrexex2  6001  f1oiso  6071  f1oiso2  6072  f1oweALT  6074  grprinvlem  6285  recseq  6634  tfrlem3  6638  tfrlem3a  6639  tfrlem12  6650  seqomlem2  6708  nneob  6895  qseq2  6955  elqsg  6956  elixpsn  7101  ixpsnf1o  7102  isfi  7131  enfi  7325  pssnn  7327  frfi  7352  unblem1  7359  unblem2  7360  unbnn2  7364  fofinf1o  7387  finsschain  7413  indexfi  7414  elfi  7418  marypha1lem  7438  supeq3  7454  supmo  7457  suplub  7465  supisolem  7475  oieq1  7481  ordtypelem2  7488  ordtypelem3  7489  ordtypelem9  7495  wemaplem1  7515  brwdom2  7541  brwdom3  7550  unwdomg  7552  oemapval  7639  cantnf  7649  wemapwe  7654  cnfcom3clem  7662  tz9.13  7717  tz9.13g  7718  cardf2  7830  isnum2  7832  ennum  7834  cardiun  7869  infxpenc2  7903  aceq1  7998  aceq2  8000  dfac5lem3  8006  dfac5lem4  8007  dfac2a  8010  dfac2  8011  kmlem9  8038  kmlem12  8041  kmlem14  8043  ackbij1  8118  cflm  8130  cfss  8145  cofsmo  8149  cfsmolem  8150  cfcoflem  8152  coftr  8153  isfin7  8181  fin23lem26  8205  isf32lem5  8237  fin1a2lem11  8290  hsmexlem2  8307  axdc3lem3  8332  axdc3  8334  numthcor  8374  zorn2lem7  8382  brdom3  8406  brdom7disj  8409  brdom6disj  8410  iundom2g  8415  fpwwe2  8518  winainflem  8568  winalim2  8571  inar1  8650  tskuni  8658  nqereu  8806  prnmax  8872  genpv  8876  genpnmax  8884  genpass  8886  prlem936  8924  recexsrlem  8978  map2psrpr  8985  supsrlem  8986  axrrecex  9038  axpre-sup  9044  cnegex  9247  recex  9654  fimaxre3  9957  infm3  9967  supmul1  9973  supmullem1  9974  supmullem2  9975  supmul  9976  creur  9994  creui  9995  cju  9996  nnunb  10217  arch  10218  xrsupsslem  10885  xrinfmsslem  10886  xrsupss  10887  xrinfmss  10888  xrub  10890  supxrunb1  10898  supxrunb2  10899  infmxrgelb  10913  fsequb2  11315  iswrd  11729  wrdval  11730  shftfval  11885  abs1m  12139  rexfiuz  12151  limsupbnd2  12277  clim  12288  rlim  12289  rlim2  12290  rlim0  12302  rlim0lt  12303  ello1mpt2  12316  o1lo1  12331  o1compt  12381  rlimdiv  12439  climsup  12463  sumeq1f  12482  sumeq2w  12486  cbvsum  12489  summo  12511  fsum  12514  fsumcvg3  12523  infcvgaux2i  12637  mertenslem1  12661  mertenslem2  12662  mertens  12663  divides  12854  odd2np1lem  12907  divalglem4  12916  divalglem10  12922  divalg  12923  gcdcllem3  13013  bezoutlem1  13038  exprmfct  13110  opeo  13187  omeo  13188  pythagtriplem2  13191  pythagtrip  13208  pceu  13220  pcprmpw2  13255  unbenlem  13276  4sqlem12  13324  vdwapval  13341  vdwapun  13342  vdwmc2  13347  vdwpc  13348  vdwlem2  13350  vdwlem10  13358  vdwlem13  13361  vdwnnlem1  13363  rami  13383  brssc  14014  isdrs  14391  drsdir  14392  drsdirfi  14395  isdrs2  14396  ipodrsima  14591  spwpr4  14663  gsumvalx  14774  gsumpropd  14776  gsumress  14777  grpinvex  14820  imasgrp2  14933  conjnmzb  15040  gaorb  15084  orbsta  15090  ispgp  15226  subgpgp  15231  sylow1  15237  pgpfi  15239  sylow2blem3  15256  fislw  15259  sylow3lem2  15262  lsmelvalm  15285  lsmass  15302  pj1fval  15326  pj1val  15327  pj1eu  15328  pj1id  15331  efgrelexlema  15381  efgrelexlemb  15382  efgredeu  15384  cyggeninv  15493  cygabl  15500  pgpfac1lem2  15633  pgpfac1lem3  15635  pgpfac1lem4  15636  pgpfac1  15638  pgpfaclem2  15640  pgpfac  15642  dvdsrval  15750  dvdsr  15751  subrgdvds  15882  lss1d  16039  lspsn  16078  lspsnel  16079  lspsolvlem  16214  rspsn  16325  opsrval  16535  znf1o  16832  cygznlem3  16850  basis2  17016  eltg2  17023  tg2  17030  isclo  17151  neival  17166  isnei  17167  isneip  17169  restbas  17222  neitr  17244  cnpval  17300  iscnp  17301  cnpimaex  17320  lmbr  17322  lmbr2  17323  cnprest2  17354  lmff  17365  regsep  17398  pnrmopn  17407  nrmsep3  17419  isnrm2  17422  iscmp  17451  cmpsublem  17462  cmpsub  17463  tgcmp  17464  sscmp  17468  hauscmplem  17469  1stcclb  17507  1stcfb  17508  is2ndc  17509  2ndc1stc  17514  1stcrest  17516  2ndcctbss  17518  1stcelcls  17524  llyeq  17533  nllyeq  17534  hausllycmp  17557  lly1stc  17559  txbas  17599  ptval  17602  ptpjopn  17644  ptclsg  17647  txcnp  17652  ptcnp  17654  txrest  17663  ptrescn  17671  txcmp  17675  tx1stc  17682  xkococn  17692  kqreglem1  17773  fbasssin  17868  fbssfi  17869  fbssint  17870  fbun  17872  fgss2  17906  fgcl  17910  ufli  17946  fmfnfmlem3  17988  fbflim2  18009  hauspwpwf1  18019  flfneii  18024  flftg  18028  txflf  18038  fclscf  18057  alexsubb  18077  alexsubALT  18082  tsmssubm  18172  ustincl  18237  ustdiag  18238  ustinvel  18239  ustexhalf  18240  ust0  18249  trust  18259  elutop  18263  ucnval  18307  ucncn  18315  cfiluexsm  18320  cfiluweak  18325  blssps  18454  blss  18455  imasf1oxms  18519  mopni  18522  metss  18538  metrest  18554  metcnp3  18570  cfilucfilOLD  18599  cfilucfil  18600  metuel2  18609  nlmvscn  18723  nrginvrcn  18727  icccmplem1  18853  icccmplem2  18854  icccmp  18856  divcn  18898  cncfval  18918  elcncf2  18920  cncfmet  18938  cnheibor  18980  evth  18984  lebnumlem3  18988  lebnum  18989  xlebnum  18990  lebnumii  18991  ipcn  19200  lmmbr  19211  lmmbr2  19212  cfilfval  19217  cfili  19221  iscfil3  19226  caufval  19228  iscau  19229  iscau2  19230  equivcfil  19252  equivcau  19253  lmcau  19265  ovolval  19370  elovolm  19371  ovolgelb  19376  ovoliunlem1  19398  ovoliun2  19402  ovolshftlem1  19405  ovolscalem1  19409  ovolicc  19419  ioombl1lem4  19455  uniioombllem2  19475  mbfaddlem  19552  mbfsup  19556  mbfinf  19557  mbflimsup  19558  i1fmulc  19595  itg1climres  19606  itg2val  19620  itg2l  19621  itg2leub  19626  itg2seq  19634  itg2monolem1  19642  itg2mono  19645  itg2i1fseq2  19648  cniccibl  19732  ellimc3  19766  limciun  19781  dvferm1  19869  dvferm2  19871  lhop1lem  19897  ply1divex  20059  ig1peu  20094  plyval  20112  elply2  20115  coeval  20142  coeeu  20144  coelem  20145  coeeq  20146  plydivlem4  20213  plydivex  20214  aannenlem2  20246  aalioulem2  20250  aaliou2  20257  ulmval  20296  ulm2  20301  ulmcau  20311  ulmdvlem3  20318  abelthlem9  20356  abelth  20357  efif1olem4  20447  eflogeq  20496  efopn  20549  cxpcn3  20632  cxpeq  20641  rlimcnp  20804  muval  20915  dchrptlem1  21048  dchrptlem2  21049  lgsdchrval  21131  pntpbnd  21282  pntibndlem3  21286  pntibnd  21287  pntlemi  21298  pntleme  21302  pntlemp  21304  pnt3  21306  nbgraf1olem1  21451  cusgrafilem2  21489  cusgrafi  21491  iseupa  21687  isgrpo  21784  isgrpoi  21786  grpoidinvlem3  21794  grpoideu  21797  grpoidinv2  21806  isgrp2d  21823  isgrpda  21885  ghgrp  21956  rngoid  21971  nmoofval  22263  nmooval  22264  nmosetn0  22266  nmoolb  22272  nmoubi  22273  nmlno0lem  22294  chcompl  22745  pjhthmo  22804  pjhval  22899  pjpreeq  22900  h1de2ci  23058  elspansn  23068  nmopval  23359  nmopsetn0  23368  nmfnval  23379  nmfnsetn0  23381  eigvecval  23399  hhcno  23407  hhcnf  23408  nmoplb  23410  nmopub  23411  nmfnlb  23427  nmfnleub  23428  eleigvec  23460  nmlnop0iALT  23498  nmopun  23517  nmcexi  23529  branmfn  23608  pjnmopi  23651  cvbr  23785  hatomic  23863  chrelat2  23873  cdjreui  23935  cdj3lem2  23938  reuxfr4d  23977  elabreximd  23991  unipreima  24056  abfmpunirn  24064  curry2ima  24097  toslub  24191  tosglb  24192  pstmfval  24291  tpr2rico  24310  rge0scvg  24335  esumc  24446  esumpcvgval  24468  dya2icoseg2  24628  dya2iocuni  24633  lgamgulmlem6  24818  subfacp1lem3  24868  pconcn  24911  cnpcon  24917  txpcon  24919  conpcon  24922  iscvm  24946  cvmcov  24950  cvmopnlem  24965  cvmliftlem15  24985  cvmlift3lem2  25007  cvmlift3lem4  25009  cvmlift3  25015  dedekind  25187  prodeq1f  25234  prodeq2w  25238  prodmo  25262  fprod  25267  br8  25379  br6  25380  br4  25381  dfrdg2  25423  dfrdg3  25424  orderseqlem  25527  poseq  25528  soseq  25529  elno  25601  sltval  25602  nobndlem6  25652  nofulllem1  25657  nofulllem2  25658  nofulllem5  25661  altxpeq2  25819  brbtwn  25838  brcgr  25839  axpasch  25880  axlowdim2  25899  axlowdim  25900  axcontlem2  25904  axcontlem4  25906  axcontlem7  25909  axcontlem8  25910  funtransport  25965  fvtransport  25966  brcolinear2  25992  colineardim1  25995  segcon2  26039  brsegle  26042  funray  26074  fvray  26075  funline  26076  linedegen  26077  fvline  26078  ellines  26086  supaddc  26237  supadd  26238  mblfinlem1  26243  mblfinlem3  26245  mblfinlem4  26246  ismblfin  26247  itg2addnclem  26256  itg2addnclem3  26258  itg2addnc  26259  itg2gt0cn  26260  cnicciblnc  26276  ftc1anclem6  26285  gtinf  26322  nn0prpwlem  26325  refssex  26361  fnessref  26373  islocfin  26376  locfinnei  26382  comppfsc  26387  neibastop2lem  26389  neibastop2  26390  tailfb  26406  unirep  26414  indexa  26435  sdclem2  26446  sdclem1  26447  sdc  26448  fdc  26449  fdc1  26450  incsequz  26452  istotbnd  26478  sstotbnd2  26483  equivtotbnd  26487  isbnd  26489  bndss  26495  ssbnd  26497  totbndbnd  26498  ismtybndlem  26515  heibor1lem  26518  heiborlem1  26520  heiborlem6  26525  heiborlem8  26527  heiborlem10  26529  heibor  26530  isdrngo2  26574  divrngidl  26638  prnc  26677  isfldidl  26678  prtlem5  26705  prtlem13  26717  prtlem16  26718  elrfi  26748  isnacs  26758  nacsfg  26759  nacsfix  26766  mzpcompact2lem  26808  eldiophb  26815  eldioph  26816  eldioph2  26820  eldioph2b  26821  eldioph3  26824  eldiophss  26833  diophrex  26834  sbc2rexg  26844  rexrabdioph  26854  rexfrabdioph  26855  elnn0rabdioph  26863  dvdsrabdioph  26870  eldioph4b  26872  eldioph4i  26873  diophren  26874  rencldnfilem  26881  pell1234qrdich  26924  jm2.27  27079  expdiophlem1  27092  wepwsolem  27116  aomclem8  27136  ellspd  27231  islnr3  27296  lnr2i  27297  lpirlnr  27298  hbtlem1  27304  hbtlem2  27305  hbtlem7  27306  hbtlem4  27307  hbtlem5  27309  hbtlem6  27310  dgraaval  27326  dgraalem  27327  dgraaub  27330  rngunsnply  27355  psgnunilem3  27396  psgneu  27406  psgnval  27407  psgnvali  27408  psgnvalii  27409  infrglb  27698  climinf  27708  climinff  27713  stoweidlem27  27752  stoweidlem31  27756  stoweidlem43  27768  stoweidlem46  27771  stoweidlem52  27777  stoweidlem60  27785  cbvrex2  27927  afvelrnb  28003  afvelrnb0  28004  el2xptp  28060  cshword  28235  cshwsiun  28286  cshwssizesame  28288  el2wlksot  28347  el2pthsot  28348  2wot2wont  28353  2spot2iun2spont  28358  frgra2v  28389  3cyclfrgrarn1  28402  frgrancvvdeqlem4  28422  bnj66  29231  bnj873  29295  bnj18eq1  29298  bnj1234  29382  bnj1318  29394  islshp  29777  lsmsat  29806  lcvbr  29819  lsatcv0  29829  lshpsmreu  29907  lshpkrlem1  29908  lshpkrlem2  29909  lshpkrlem3  29910  lshpkrcl  29914  lshpset2N  29917  islshpkrN  29918  cvrval  30067  atlex  30114  glbconxN  30175  hlsuprexch  30178  islln  30303  islpln  30327  islpln5  30332  lvolex3N  30335  islvol  30370  islvol5  30376  ispointN  30539  pmapglbx  30566  paddval  30595  elpaddn0  30597  elpaddat  30601  elpadd0  30606  4atex  30873  4atex2  30874  cdlemefrs29bpre1  31194  cdlemefrs32fva  31197  cdlemg33b  31504  dvhb1dimN  31783  dvhopellsm  31915  dib1dim  31963  diclspsn  31992  dihglblem2aN  32091  dihglblem2N  32092  dih1dimatlem  32127  dvh3dimatN  32237  dvh2dim  32243  dvh3dim  32244  dvh4dimN  32245  dvh3dim3N  32247  dochfl1  32274  lcfl7N  32299  lcf1o  32349  lcfrlem39  32379  mapdpglem3  32473  hvmapvalvalN  32559  hdmap14lem2a  32668  hdmapglem7a  32728
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-11 1761
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1551  df-nf 1554  df-rex 2711
  Copyright terms: Public domain W3C validator