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

Theorem rexbidv 2577
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 1609 . 2  |-  F/ x ph
2 ralbidv.1 . 2  |-  ( ph  ->  ( ps  <->  ch )
)
31, 2rexbid 2575 1  |-  ( ph  ->  ( E. x  e.  A  ps  <->  E. x  e.  A  ch )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176   E.wrex 2557
This theorem is referenced by:  rexbii  2581  2rexbidv  2599  rexralbidv  2600  rexeqbi1dv  2758  rexeqbidv  2762  cbvrex2v  2786  rspc2ev  2905  rspc3ev  2907  ceqsrex2v  2916  sbcrexg  3079  uniiunlem  3273  eliun  3925  dfiin2g  3952  orduninsuc  4650  elrnmpt  4942  elrnmptg  4945  elimag  5032  funcnvuni  5333  fun11iun  5509  fvelrnb  5586  fvelimab  5594  foelrn  5695  foco2  5696  elabrex  5781  abrexco  5782  abrexex2g  5784  abrexex2  5796  f1oiso  5864  f1oiso2  5865  f1oweALT  5867  grprinvlem  6074  recseq  6405  tfrlem3  6409  tfrlem3a  6410  tfrlem12  6421  seqomlem2  6479  nneob  6666  qseq2  6726  elqsg  6727  elixpsn  6871  ixpsnf1o  6872  isfi  6901  enfi  7095  pssnn  7097  frfi  7118  unblem1  7125  unblem2  7126  unbnn2  7130  fofinf1o  7153  finsschain  7178  indexfi  7179  elfi  7183  marypha1lem  7202  supmo  7219  suplub  7227  supisolem  7237  oieq1  7243  ordtypelem2  7250  ordtypelem3  7251  ordtypelem9  7257  wemaplem1  7277  brwdom2  7303  brwdom3  7312  unwdomg  7314  oemapval  7401  cantnf  7411  wemapwe  7416  cnfcom3clem  7424  tz9.13  7479  tz9.13g  7480  cardf2  7592  isnum2  7594  ennum  7596  cardiun  7631  infxpenc2  7665  aceq1  7760  aceq2  7762  dfac5lem3  7768  dfac5lem4  7769  dfac2a  7772  dfac2  7773  kmlem9  7800  kmlem12  7803  kmlem14  7805  ackbij1  7880  cflm  7892  cfss  7907  cofsmo  7911  cfsmolem  7912  cfcoflem  7914  coftr  7915  isfin7  7943  fin23lem26  7967  isf32lem5  7999  fin1a2lem11  8052  hsmexlem2  8069  axdc3lem3  8094  axdc3  8096  numthcor  8137  zorn2lem7  8145  brdom3  8169  brdom7disj  8172  brdom6disj  8173  iundom2g  8178  fpwwe2  8281  winainflem  8331  winalim2  8334  inar1  8413  tskuni  8421  nqereu  8569  prnmax  8635  genpv  8639  genpnmax  8647  genpass  8649  prlem936  8687  recexsrlem  8741  map2psrpr  8748  supsrlem  8749  axrrecex  8801  axpre-sup  8807  cnegex  9009  recex  9416  fimaxre3  9719  infm3  9729  supmul1  9735  supmullem1  9736  supmullem2  9737  supmul  9738  creur  9756  creui  9757  cju  9758  nnunb  9977  arch  9978  xrsupsslem  10641  xrinfmsslem  10642  xrsupss  10643  xrinfmss  10644  xrub  10646  supxrunb1  10654  supxrunb2  10655  infmxrgelb  10669  fsequb2  11054  iswrd  11431  wrdval  11432  shftfval  11581  abs1m  11835  rexfiuz  11847  limsupbnd2  11973  clim  11984  rlim  11985  rlim2  11986  rlim0  11998  rlim0lt  11999  ello1mpt2  12012  o1lo1  12027  o1compt  12077  rlimdiv  12135  climsup  12159  sumeq1f  12177  sumeq2w  12181  cbvsum  12184  summo  12206  fsum  12209  fsumcvg3  12218  infcvgaux2i  12332  mertenslem1  12356  mertenslem2  12357  mertens  12358  divides  12549  odd2np1lem  12602  divalglem4  12611  divalglem10  12617  divalg  12618  gcdcllem3  12708  bezoutlem1  12733  exprmfct  12805  opeo  12882  omeo  12883  pythagtriplem2  12886  pythagtrip  12903  pceu  12915  pcprmpw2  12950  unbenlem  12971  4sqlem12  13019  vdwapval  13036  vdwapun  13037  vdwmc2  13042  vdwpc  13043  vdwlem2  13045  vdwlem10  13053  vdwlem13  13056  vdwnnlem1  13058  rami  13078  brssc  13707  isdrs  14084  drsdir  14085  drsdirfi  14088  isdrs2  14089  ipodrsima  14284  spwpr4  14356  gsumvalx  14467  gsumpropd  14469  gsumress  14470  grpinvex  14513  imasgrp2  14626  conjnmzb  14733  gaorb  14777  orbsta  14783  ispgp  14919  subgpgp  14924  sylow1  14930  pgpfi  14932  sylow2blem3  14949  fislw  14952  sylow3lem2  14955  lsmelvalm  14978  lsmass  14995  pj1fval  15019  pj1val  15020  pj1eu  15021  pj1id  15024  efgrelexlema  15074  efgrelexlemb  15075  efgredeu  15077  cyggeninv  15186  cygabl  15193  pgpfac1lem2  15326  pgpfac1lem3  15328  pgpfac1lem4  15329  pgpfac1  15331  pgpfaclem2  15333  pgpfac  15335  dvdsrval  15443  dvdsr  15444  subrgdvds  15575  lss1d  15736  lspsn  15775  lspsnel  15776  lspsolvlem  15911  rspsn  16022  opsrval  16232  znf1o  16521  cygznlem3  16539  basis2  16705  eltg2  16712  tg2  16719  isclo  16840  neival  16855  isnei  16856  isneip  16858  restbas  16905  cnpval  16982  iscnp  16983  cnpimaex  17002  lmbr  17004  lmbr2  17005  cnprest2  17034  lmff  17045  regsep  17078  pnrmopn  17087  nrmsep3  17099  isnrm2  17102  iscmp  17131  cmpsublem  17142  cmpsub  17143  tgcmp  17144  sscmp  17148  hauscmplem  17149  1stcclb  17186  1stcfb  17187  is2ndc  17188  2ndc1stc  17193  1stcrest  17195  2ndcctbss  17197  1stcelcls  17203  llyeq  17212  nllyeq  17213  hausllycmp  17236  lly1stc  17238  txbas  17278  ptval  17281  ptpjopn  17322  ptclsg  17325  txcnp  17330  ptcnp  17332  txrest  17341  ptrescn  17349  txcmp  17353  tx1stc  17360  xkococn  17370  kqreglem1  17448  fbasssin  17547  fbssfi  17548  fbssint  17549  fbun  17551  fgss2  17585  fgcl  17589  ufli  17625  fmfnfmlem3  17667  fbflim2  17688  hauspwpwf1  17698  flfneii  17703  flftg  17707  txflf  17717  fclscf  17736  alexsubb  17756  alexsubALT  17761  tsmssubm  17841  blss  17988  imasf1oxms  18051  mopni  18054  metss  18070  metrest  18086  metcnp3  18102  nlmvscn  18214  nrginvrcn  18218  icccmplem1  18343  icccmplem2  18344  icccmp  18346  divcn  18388  cncfval  18408  elcncf2  18410  cncfmet  18428  cnheibor  18469  evth  18473  lebnumlem3  18477  lebnum  18478  xlebnum  18479  lebnumii  18480  ipcn  18689  lmmbr  18700  lmmbr2  18701  cfilfval  18706  cfili  18710  iscfil3  18715  caufval  18717  iscau  18718  iscau2  18719  equivcfil  18741  equivcau  18742  lmcau  18754  ovolval  18849  elovolm  18850  ovolgelb  18855  ovoliunlem1  18877  ovoliun2  18881  ovolshftlem1  18884  ovolscalem1  18888  ovolicc  18898  ioombl1lem4  18934  uniioombllem2  18954  mbfaddlem  19031  mbfsup  19035  mbfinf  19036  mbflimsup  19037  i1fmulc  19074  itg1climres  19085  itg2val  19099  itg2l  19100  itg2leub  19105  itg2seq  19113  itg2monolem1  19121  itg2mono  19124  itg2i1fseq2  19127  cniccibl  19211  ellimc3  19245  limciun  19260  dvferm1  19348  dvferm2  19350  lhop1lem  19376  ply1divex  19538  ig1peu  19573  plyval  19591  elply2  19594  coeval  19621  coeeu  19623  coelem  19624  coeeq  19625  plydivlem4  19692  plydivex  19693  aannenlem2  19725  aalioulem2  19729  aaliou2  19736  ulmval  19775  ulm2  19780  ulmcau  19788  ulmdvlem3  19795  abelthlem9  19832  abelth  19833  efif1olem4  19923  eflogeq  19971  efopn  20021  cxpcn3  20104  cxpeq  20113  rlimcnp  20276  muval  20386  dchrptlem1  20519  dchrptlem2  20520  lgsdchrval  20602  pntpbnd  20753  pntibndlem3  20757  pntibnd  20758  pntlemi  20769  pntleme  20773  pntlemp  20775  pnt3  20777  isgrpo  20879  isgrpoi  20881  grpoidinvlem3  20889  grpoideu  20892  grpoidinv2  20901  isgrp2d  20918  isgrpda  20980  ghgrp  21051  rngoid  21066  nmoofval  21356  nmooval  21357  nmosetn0  21359  nmoolb  21365  nmoubi  21366  nmlno0lem  21387  chcompl  21838  pjhthmo  21897  pjhval  21992  pjpreeq  21993  h1de2ci  22151  elspansn  22161  nmopval  22452  nmopsetn0  22461  nmfnval  22472  nmfnsetn0  22474  eigvecval  22492  hhcno  22500  hhcnf  22501  nmoplb  22503  nmopub  22504  nmfnlb  22520  nmfnleub  22521  eleigvec  22553  nmlnop0iALT  22591  nmopun  22610  nmcexi  22622  branmfn  22701  pjnmopi  22744  cvbr  22878  hatomic  22956  chrelat2  22966  cdjreui  23028  cdj3lem2  23031  reuxfr4d  23155  unipreima  23224  abfmpunirn  23231  curry2ima  23262  tpr2rico  23311  rge0scvg  23388  esumpcvgval  23461  dya2iocseg  23594  subfacp1lem3  23728  pconcn  23770  cnpcon  23776  txpcon  23778  conpcon  23781  iscvm  23805  cvmcov  23809  cvmopnlem  23824  cvmliftlem15  23844  cvmlift3lem2  23866  cvmlift3lem4  23868  cvmlift3  23874  iseupa  23896  dedekind  24097  cprodeq1f  24130  cprodeq2w  24134  prodmo  24159  fprod  24164  br8  24184  br6  24185  br4  24186  dfrdg2  24223  dfrdg3  24224  orderseqlem  24323  poseq  24324  soseq  24325  elno  24371  sltval  24372  nobndlem6  24422  nofulllem1  24427  nofulllem2  24428  nofulllem5  24431  altxpeq2  24580  brbtwn  24599  brcgr  24600  axpasch  24641  axlowdim2  24660  axlowdim  24661  axcontlem2  24665  axcontlem4  24667  axcontlem7  24670  axcontlem8  24671  funtransport  24726  fvtransport  24727  brcolinear2  24753  colineardim1  24756  segcon2  24800  brsegle  24803  funray  24835  fvray  24836  funline  24837  linedegen  24838  fvline  24839  ellines  24847  supaddc  24995  supadd  24996  itg2addnclem  25003  itg2addnc  25005  itg2gt0cn  25006  cnicciblnc  25022  ab2rexexg  25225  nZdef  25283  prodeq1  25409  prodeq2  25410  mgmlion  25440  prsubrtr  25502  basexre  25625  sallnei  25632  efilcp  25655  fgsb2  25658  cnfilca  25659  limptlimpr2lem1  25677  limptlimpr2lem2  25678  tcnvec  25793  isfunb  25938  vtarsuelt  25998  dfiunv2  26019  fnckle  26148  cndpv  26152  pgapspf  26155  iscol2  26196  isibg2  26213  isibg2aa  26215  isibg2aalem1  26216  isibcg  26294  gtinf  26337  nn0prpwlem  26341  refssex  26384  fnessref  26396  islocfin  26399  locfinnei  26405  comppfsc  26410  neibastop2lem  26412  neibastop2  26413  tailfb  26429  unirep  26452  indexa  26515  sdclem2  26555  sdclem1  26556  sdc  26557  fdc  26558  fdc1  26559  incsequz  26561  istotbnd  26596  sstotbnd2  26601  equivtotbnd  26605  isbnd  26607  bndss  26613  ssbnd  26615  totbndbnd  26616  ismtybndlem  26633  heibor1lem  26636  heiborlem1  26638  heiborlem6  26643  heiborlem8  26645  heiborlem10  26647  heibor  26648  isdrngo2  26692  divrngidl  26756  prnc  26795  isfldidl  26796  prtlem5  26825  prtlem13  26839  prtlem16  26840  elrfi  26872  isnacs  26882  nacsfg  26883  nacsfix  26890  mzpcompact2lem  26932  eldiophb  26939  eldioph  26940  eldioph2  26944  eldioph2b  26945  eldioph3  26948  eldiophss  26957  diophrex  26958  sbc2rexg  26968  rexrabdioph  26978  rexfrabdioph  26979  elnn0rabdioph  26987  dvdsrabdioph  26994  eldioph4b  26997  eldioph4i  26998  diophren  26999  rencldnfilem  27006  pell1234qrdich  27049  jm2.27  27204  expdiophlem1  27217  wepwsolem  27241  aomclem8  27262  ellspd  27357  islnr3  27422  lnr2i  27423  lpirlnr  27424  hbtlem1  27430  hbtlem2  27431  hbtlem7  27432  hbtlem4  27433  hbtlem5  27435  hbtlem6  27436  dgraaval  27452  dgraalem  27453  dgraaub  27456  rngunsnply  27481  psgnunilem3  27522  psgneu  27532  psgnval  27533  psgnvali  27534  psgnvalii  27535  infrglb  27825  climinf  27835  climinff  27840  stoweidlem27  27879  stoweidlem31  27883  stoweidlem43  27895  stoweidlem46  27898  stoweidlem52  27904  cbvrex2  28054  afvelrnb  28131  afvelrnb0  28132  frgra2v  28423  3cyclfrgrarn1  28435  bnj66  29208  bnj873  29272  bnj18eq1  29275  bnj1234  29359  bnj1318  29371  islshp  29791  lsmsat  29820  lcvbr  29833  lsatcv0  29843  lshpsmreu  29921  lshpkrlem1  29922  lshpkrlem2  29923  lshpkrlem3  29924  lshpkrcl  29928  lshpset2N  29931  islshpkrN  29932  cvrval  30081  atlex  30128  glbconxN  30189  hlsuprexch  30192  islln  30317  islpln  30341  islpln5  30346  lvolex3N  30349  islvol  30384  islvol5  30390  ispointN  30553  pmapglbx  30580  paddval  30609  elpaddn0  30611  elpaddat  30615  elpadd0  30620  4atex  30887  4atex2  30888  cdlemefrs29bpre1  31208  cdlemefrs32fva  31211  cdlemg33b  31518  dvhb1dimN  31797  dvhopellsm  31929  dib1dim  31977  diclspsn  32006  dihglblem2aN  32105  dihglblem2N  32106  dih1dimatlem  32141  dvh3dimatN  32251  dvh2dim  32257  dvh3dim  32258  dvh4dimN  32259  dvh3dim3N  32261  dochfl1  32288  lcfl7N  32313  lcf1o  32363  lcfrlem39  32393  mapdpglem3  32487  hvmapvalvalN  32573  hdmap14lem2a  32682  hdmapglem7a  32742
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-11 1727
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1532  df-nf 1535  df-rex 2562
  Copyright terms: Public domain W3C validator