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

Theorem rexbidv 2564
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 1605 . 2  |-  F/ x ph
2 ralbidv.1 . 2  |-  ( ph  ->  ( ps  <->  ch )
)
31, 2rexbid 2562 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 2544
This theorem is referenced by:  rexbii  2568  2rexbidv  2586  rexralbidv  2587  rexeqbi1dv  2745  rexeqbidv  2749  cbvrex2v  2773  rspc2ev  2892  rspc3ev  2894  ceqsrex2v  2903  sbcrexg  3066  uniiunlem  3260  eliun  3909  dfiin2g  3936  orduninsuc  4634  elrnmpt  4926  elrnmptg  4929  elimag  5016  funcnvuni  5317  fun11iun  5493  fvelrnb  5570  fvelimab  5578  foelrn  5679  foco2  5680  elabrex  5765  abrexco  5766  abrexex2g  5768  abrexex2  5780  f1oiso  5848  f1oiso2  5849  f1oweALT  5851  grprinvlem  6058  recseq  6389  tfrlem3  6393  tfrlem3a  6394  tfrlem12  6405  seqomlem2  6463  nneob  6650  qseq2  6710  elqsg  6711  elixpsn  6855  ixpsnf1o  6856  isfi  6885  enfi  7079  pssnn  7081  frfi  7102  unblem1  7109  unblem2  7110  unbnn2  7114  fofinf1o  7137  finsschain  7162  indexfi  7163  elfi  7167  marypha1lem  7186  supmo  7203  suplub  7211  supisolem  7221  oieq1  7227  ordtypelem2  7234  ordtypelem3  7235  ordtypelem9  7241  wemaplem1  7261  brwdom2  7287  brwdom3  7296  unwdomg  7298  oemapval  7385  cantnf  7395  wemapwe  7400  cnfcom3clem  7408  tz9.13  7463  tz9.13g  7464  cardf2  7576  isnum2  7578  ennum  7580  cardiun  7615  infxpenc2  7649  aceq1  7744  aceq2  7746  dfac5lem3  7752  dfac5lem4  7753  dfac2a  7756  dfac2  7757  kmlem9  7784  kmlem12  7787  kmlem14  7789  ackbij1  7864  cflm  7876  cfss  7891  cofsmo  7895  cfsmolem  7896  cfcoflem  7898  coftr  7899  isfin7  7927  fin23lem26  7951  isf32lem5  7983  fin1a2lem11  8036  hsmexlem2  8053  axdc3lem3  8078  axdc3  8080  numthcor  8121  zorn2lem7  8129  brdom3  8153  brdom7disj  8156  brdom6disj  8157  iundom2g  8162  fpwwe2  8265  winainflem  8315  winalim2  8318  inar1  8397  tskuni  8405  nqereu  8553  prnmax  8619  genpv  8623  genpnmax  8631  genpass  8633  prlem936  8671  recexsrlem  8725  map2psrpr  8732  supsrlem  8733  axrrecex  8785  axpre-sup  8791  cnegex  8993  recex  9400  fimaxre3  9703  infm3  9713  supmul1  9719  supmullem1  9720  supmullem2  9721  supmul  9722  creur  9740  creui  9741  cju  9742  nnunb  9961  arch  9962  xrsupsslem  10625  xrinfmsslem  10626  xrsupss  10627  xrinfmss  10628  xrub  10630  supxrunb1  10638  supxrunb2  10639  infmxrgelb  10653  fsequb2  11038  iswrd  11415  wrdval  11416  shftfval  11565  abs1m  11819  rexfiuz  11831  limsupbnd2  11957  clim  11968  rlim  11969  rlim2  11970  rlim0  11982  rlim0lt  11983  ello1mpt2  11996  o1lo1  12011  o1compt  12061  rlimdiv  12119  climsup  12143  sumeq1f  12161  sumeq2w  12165  cbvsum  12168  summo  12190  fsum  12193  fsumcvg3  12202  infcvgaux2i  12316  mertenslem1  12340  mertenslem2  12341  mertens  12342  divides  12533  odd2np1lem  12586  divalglem4  12595  divalglem10  12601  divalg  12602  gcdcllem3  12692  bezoutlem1  12717  exprmfct  12789  opeo  12866  omeo  12867  pythagtriplem2  12870  pythagtrip  12887  pceu  12899  pcprmpw2  12934  unbenlem  12955  4sqlem12  13003  vdwapval  13020  vdwapun  13021  vdwmc2  13026  vdwpc  13027  vdwlem2  13029  vdwlem10  13037  vdwlem13  13040  vdwnnlem1  13042  rami  13062  brssc  13691  isdrs  14068  drsdir  14069  drsdirfi  14072  isdrs2  14073  ipodrsima  14268  spwpr4  14340  gsumvalx  14451  gsumpropd  14453  gsumress  14454  grpinvex  14497  imasgrp2  14610  conjnmzb  14717  gaorb  14761  orbsta  14767  ispgp  14903  subgpgp  14908  sylow1  14914  pgpfi  14916  sylow2blem3  14933  fislw  14936  sylow3lem2  14939  lsmelvalm  14962  lsmass  14979  pj1fval  15003  pj1val  15004  pj1eu  15005  pj1id  15008  efgrelexlema  15058  efgrelexlemb  15059  efgredeu  15061  cyggeninv  15170  cygabl  15177  pgpfac1lem2  15310  pgpfac1lem3  15312  pgpfac1lem4  15313  pgpfac1  15315  pgpfaclem2  15317  pgpfac  15319  dvdsrval  15427  dvdsr  15428  subrgdvds  15559  lss1d  15720  lspsn  15759  lspsnel  15760  lspsolvlem  15895  rspsn  16006  opsrval  16216  znf1o  16505  cygznlem3  16523  basis2  16689  eltg2  16696  tg2  16703  isclo  16824  neival  16839  isnei  16840  isneip  16842  restbas  16889  cnpval  16966  iscnp  16967  cnpimaex  16986  lmbr  16988  lmbr2  16989  cnprest2  17018  lmff  17029  regsep  17062  pnrmopn  17071  nrmsep3  17083  isnrm2  17086  iscmp  17115  cmpsublem  17126  cmpsub  17127  tgcmp  17128  sscmp  17132  hauscmplem  17133  1stcclb  17170  1stcfb  17171  is2ndc  17172  2ndc1stc  17177  1stcrest  17179  2ndcctbss  17181  1stcelcls  17187  llyeq  17196  nllyeq  17197  hausllycmp  17220  lly1stc  17222  txbas  17262  ptval  17265  ptpjopn  17306  ptclsg  17309  txcnp  17314  ptcnp  17316  txrest  17325  ptrescn  17333  txcmp  17337  tx1stc  17344  xkococn  17354  kqreglem1  17432  fbasssin  17531  fbssfi  17532  fbssint  17533  fbun  17535  fgss2  17569  fgcl  17573  ufli  17609  fmfnfmlem3  17651  fbflim2  17672  hauspwpwf1  17682  flfneii  17687  flftg  17691  txflf  17701  fclscf  17720  alexsubb  17740  alexsubALT  17745  tsmssubm  17825  blss  17972  imasf1oxms  18035  mopni  18038  metss  18054  metrest  18070  metcnp3  18086  nlmvscn  18198  nrginvrcn  18202  icccmplem1  18327  icccmplem2  18328  icccmp  18330  divcn  18372  cncfval  18392  elcncf2  18394  cncfmet  18412  cnheibor  18453  evth  18457  lebnumlem3  18461  lebnum  18462  xlebnum  18463  lebnumii  18464  ipcn  18673  lmmbr  18684  lmmbr2  18685  cfilfval  18690  cfili  18694  iscfil3  18699  caufval  18701  iscau  18702  iscau2  18703  equivcfil  18725  equivcau  18726  lmcau  18738  ovolval  18833  elovolm  18834  ovolgelb  18839  ovoliunlem1  18861  ovoliun2  18865  ovolshftlem1  18868  ovolscalem1  18872  ovolicc  18882  ioombl1lem4  18918  uniioombllem2  18938  mbfaddlem  19015  mbfsup  19019  mbfinf  19020  mbflimsup  19021  i1fmulc  19058  itg1climres  19069  itg2val  19083  itg2l  19084  itg2leub  19089  itg2seq  19097  itg2monolem1  19105  itg2mono  19108  itg2i1fseq2  19111  cniccibl  19195  ellimc3  19229  limciun  19244  dvferm1  19332  dvferm2  19334  lhop1lem  19360  ply1divex  19522  ig1peu  19557  plyval  19575  elply2  19578  coeval  19605  coeeu  19607  coelem  19608  coeeq  19609  plydivlem4  19676  plydivex  19677  aannenlem2  19709  aalioulem2  19713  aaliou2  19720  ulmval  19759  ulm2  19764  ulmcau  19772  ulmdvlem3  19779  abelthlem9  19816  abelth  19817  efif1olem4  19907  eflogeq  19955  efopn  20005  cxpcn3  20088  cxpeq  20097  rlimcnp  20260  muval  20370  dchrptlem1  20503  dchrptlem2  20504  lgsdchrval  20586  pntpbnd  20737  pntibndlem3  20741  pntibnd  20742  pntlemi  20753  pntleme  20757  pntlemp  20759  pnt3  20761  isgrpo  20863  isgrpoi  20865  grpoidinvlem3  20873  grpoideu  20876  grpoidinv2  20885  isgrp2d  20902  isgrpda  20964  ghgrp  21035  rngoid  21050  nmoofval  21340  nmooval  21341  nmosetn0  21343  nmoolb  21349  nmoubi  21350  nmlno0lem  21371  chcompl  21822  pjhthmo  21881  pjhval  21976  pjpreeq  21977  h1de2ci  22135  elspansn  22145  nmopval  22436  nmopsetn0  22445  nmfnval  22456  nmfnsetn0  22458  eigvecval  22476  hhcno  22484  hhcnf  22485  nmoplb  22487  nmopub  22488  nmfnlb  22504  nmfnleub  22505  eleigvec  22537  nmlnop0iALT  22575  nmopun  22594  nmcexi  22606  branmfn  22685  pjnmopi  22728  cvbr  22862  hatomic  22940  chrelat2  22950  cdjreui  23012  cdj3lem2  23015  reuxfr4d  23139  unipreima  23209  abfmpunirn  23216  curry2ima  23247  tpr2rico  23296  rge0scvg  23373  esumpcvgval  23446  dya2iocseg  23579  subfacp1lem3  23713  pconcn  23755  cnpcon  23761  txpcon  23763  conpcon  23766  iscvm  23790  cvmcov  23794  cvmopnlem  23809  cvmliftlem15  23829  cvmlift3lem2  23851  cvmlift3lem4  23853  cvmlift3  23859  iseupa  23881  dedekind  24082  br8  24113  br6  24114  br4  24115  dfrdg2  24152  dfrdg3  24153  orderseqlem  24252  poseq  24253  soseq  24254  elno  24300  sltval  24301  nobndlem6  24351  nofulllem1  24356  nofulllem2  24357  nofulllem5  24360  altxpeq2  24508  brbtwn  24527  brcgr  24528  axpasch  24569  axlowdim2  24588  axlowdim  24589  axcontlem2  24593  axcontlem4  24595  axcontlem7  24598  axcontlem8  24599  funtransport  24654  fvtransport  24655  brcolinear2  24681  colineardim1  24684  segcon2  24728  brsegle  24731  funray  24763  fvray  24764  funline  24765  linedegen  24766  fvline  24767  ellines  24775  ab2rexexg  25122  nZdef  25180  prodeq1  25306  prodeq2  25307  mgmlion  25337  prsubrtr  25399  basexre  25522  sallnei  25529  efilcp  25552  fgsb2  25555  cnfilca  25556  limptlimpr2lem1  25574  limptlimpr2lem2  25575  tcnvec  25690  isfunb  25835  vtarsuelt  25895  dfiunv2  25916  fnckle  26045  cndpv  26049  pgapspf  26052  iscol2  26093  isibg2  26110  isibg2aa  26112  isibg2aalem1  26113  isibcg  26191  gtinf  26234  nn0prpwlem  26238  refssex  26281  fnessref  26293  islocfin  26296  locfinnei  26302  comppfsc  26307  neibastop2lem  26309  neibastop2  26310  tailfb  26326  unirep  26349  indexa  26412  sdclem2  26452  sdclem1  26453  sdc  26454  fdc  26455  fdc1  26456  incsequz  26458  istotbnd  26493  sstotbnd2  26498  equivtotbnd  26502  isbnd  26504  bndss  26510  ssbnd  26512  totbndbnd  26513  ismtybndlem  26530  heibor1lem  26533  heiborlem1  26535  heiborlem6  26540  heiborlem8  26542  heiborlem10  26544  heibor  26545  isdrngo2  26589  divrngidl  26653  prnc  26692  isfldidl  26693  prtlem5  26722  prtlem13  26736  prtlem16  26737  elrfi  26769  isnacs  26779  nacsfg  26780  nacsfix  26787  mzpcompact2lem  26829  eldiophb  26836  eldioph  26837  eldioph2  26841  eldioph2b  26842  eldioph3  26845  eldiophss  26854  diophrex  26855  sbc2rexg  26865  rexrabdioph  26875  rexfrabdioph  26876  elnn0rabdioph  26884  dvdsrabdioph  26891  eldioph4b  26894  eldioph4i  26895  diophren  26896  rencldnfilem  26903  pell1234qrdich  26946  jm2.27  27101  expdiophlem1  27114  wepwsolem  27138  aomclem8  27159  ellspd  27254  islnr3  27319  lnr2i  27320  lpirlnr  27321  hbtlem1  27327  hbtlem2  27328  hbtlem7  27329  hbtlem4  27330  hbtlem5  27332  hbtlem6  27333  dgraaval  27349  dgraalem  27350  dgraaub  27353  rngunsnply  27378  psgnunilem3  27419  psgneu  27429  psgnval  27430  psgnvali  27431  psgnvalii  27432  infrglb  27722  climinf  27732  climinff  27737  stoweidlem27  27776  stoweidlem31  27780  stoweidlem43  27792  stoweidlem46  27795  stoweidlem52  27801  cbvrex2  27951  afvelrnb  28025  afvelrnb0  28026  frgra2v  28177  bnj66  28892  bnj873  28956  bnj18eq1  28959  bnj1234  29043  bnj1318  29055  islshp  29169  lsmsat  29198  lcvbr  29211  lsatcv0  29221  lshpsmreu  29299  lshpkrlem1  29300  lshpkrlem2  29301  lshpkrlem3  29302  lshpkrcl  29306  lshpset2N  29309  islshpkrN  29310  cvrval  29459  atlex  29506  glbconxN  29567  hlsuprexch  29570  islln  29695  islpln  29719  islpln5  29724  lvolex3N  29727  islvol  29762  islvol5  29768  ispointN  29931  pmapglbx  29958  paddval  29987  elpaddn0  29989  elpaddat  29993  elpadd0  29998  4atex  30265  4atex2  30266  cdlemefrs29bpre1  30586  cdlemefrs32fva  30589  cdlemg33b  30896  dvhb1dimN  31175  dvhopellsm  31307  dib1dim  31355  diclspsn  31384  dihglblem2aN  31483  dihglblem2N  31484  dih1dimatlem  31519  dvh3dimatN  31629  dvh2dim  31635  dvh3dim  31636  dvh4dimN  31637  dvh3dim3N  31639  dochfl1  31666  lcfl7N  31691  lcf1o  31741  lcfrlem39  31771  mapdpglem3  31865  hvmapvalvalN  31951  hdmap14lem2a  32060  hdmapglem7a  32120
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-11 1715
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1529  df-nf 1532  df-rex 2549
  Copyright terms: Public domain W3C validator