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

Theorem ralbidva 2721
Description: Formula-building rule for restricted universal quantifier (deduction rule). (Contributed by NM, 4-Mar-1997.)
Hypothesis
Ref Expression
ralbidva.1  |-  ( (
ph  /\  x  e.  A )  ->  ( ps 
<->  ch ) )
Assertion
Ref Expression
ralbidva  |-  ( ph  ->  ( A. x  e.  A  ps  <->  A. x  e.  A  ch )
)
Distinct variable group:    ph, x
Allowed substitution hints:    ps( x)    ch( x)    A( x)

Proof of Theorem ralbidva
StepHypRef Expression
1 nfv 1672 . 2  |-  F/ x ph
2 ralbidva.1 . 2  |-  ( (
ph  /\  x  e.  A )  ->  ( ps 
<->  ch ) )
31, 2ralbida 2719 1  |-  ( ph  ->  ( A. x  e.  A  ps  <->  A. x  e.  A  ch )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 369    e. wcel 1755   A.wral 2705
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-12 1791
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1590  df-nf 1593  df-ral 2710
This theorem is referenced by:  raleqbidva  2923  ordunisssuc  4808  poinxp  4889  soinxp  4890  frinxp  4891  fnmptfvd  5794  funimass3  5807  fnnfpeq0  5896  fnsuppresOLD  5925  cocan1  5982  cocan2  5983  isores2  6011  isoini2  6017  ofrfval  6317  ofrfval2  6326  tfindsg2  6461  f1oweALT  6550  fnsuppres  6705  dfsmo2  6794  smores  6799  smores2  6801  ac6sfi  7544  fimaxg  7547  ordunifi  7550  isfinite2  7558  fipreima  7605  supisolem  7708  ordiso2  7717  ordtypelem7  7726  cantnf  7889  cantnfOLD  7911  wemapwe  7916  wemapweOLD  7917  rankval3b  8021  rankonidlem  8023  iscard  8133  acndom  8209  dfac12lem3  8302  kmlem2  8308  cflim2  8420  cfsmolem  8427  ttukeylem6  8671  alephreg  8734  suplem2pr  9209  axsup  9437  sup3  10274  infm3  10276  suprleub  10281  dfinfmr  10294  infmrgelb  10297  ofsubeq0  10306  ofsubge0  10308  zextlt  10703  prime  10709  indstr  10910  supxr2  11263  supxrbnd1  11271  supxrbnd2  11272  supxrleub  11276  supxrbnd  11278  infmxrgelb  11284  fzshftral  11530  swrdeq  12323  swrdsymbeq  12324  clim  12955  rlim  12956  clim2  12965  clim2c  12966  clim0c  12968  ello1mpt  12982  lo1o1  12993  o1lo1  12998  climabs0  13046  o1compt  13048  rlimdiv  13106  geomulcvg  13318  mertenslem2  13327  mertens  13328  rpnnen2  13490  sqr2irr  13513  pc11  13928  pcz  13929  1arith  13970  vdwlem8  14031  vdwlem11  14034  vdw  14037  ramval  14051  pwsle  14412  mrieqvd  14558  mreacs  14578  cidpropd  14631  ismon2  14655  monpropd  14658  isepi  14661  isepi2  14662  subsubc  14745  funcres2b  14789  funcpropd  14792  isfull2  14803  isfth2  14807  fucsect  14864  fucinv  14865  pospropd  15286  ipodrsfi  15315  tsrss  15375  mndpropd  15428  grpidpropd  15429  grppropd  15535  issubg4  15679  gass  15798  gsmsymgrfixlem1  15911  gsmsymgreqlem2  15915  gexdvds  16062  gexdvds2  16063  subgpgp  16075  sylow3lem6  16110  efgval2  16200  efgsp1  16213  dprdf11  16486  dprdf11OLD  16493  subgdmdprd  16504  rngpropd  16611  abvpropd  16850  lsspropd  17019  lbspropd  17101  assapropd  17319  psrbaglefi  17374  psrbaglefiOLD  17375  psrbagconf1o  17377  gsumbagdiaglem  17378  mplmonmul  17476  phlpropd  17925  ishil2  17985  lindfmm  18097  islindf4  18108  islindf5  18109  tgss2  18433  isclo  18532  neips  18558  opnnei  18565  isperf3  18598  ssidcn  18700  lmbrf  18705  cnnei  18727  cnrest2  18731  lmss  18743  lmres  18745  ist1-2  18792  ist1-3  18794  isreg2  18822  cmpfi  18852  bwth  18854  1stccn  18908  subislly  18926  kgencn  18970  ptclsg  19029  ptcnplem  19035  xkococnlem  19073  xkoinjcn  19101  tgqtop  19126  qtopcn  19128  fbflim  19390  flimrest  19397  flfnei  19405  isflf  19407  cnflf  19416  fclsopn  19428  fclsbas  19435  fclsrest  19438  isfcf  19448  cnfcf  19456  ptcmplem3  19467  tmdgsum2  19508  eltsms  19544  tsmsgsum  19550  tsmsgsumOLD  19553  tsmssubm  19557  tsmsf1o  19560  utopsnneiplem  19663  ismet2  19749  prdsxmetlem  19784  elmopn2  19861  prdsbl  19907  metss  19924  metrest  19940  metcnp  19957  metcnp2  19958  metcn  19959  metucnOLD  20004  metucn  20005  nrginvrcn  20113  metdsge  20266  divcn  20285  elcncf2  20307  mulc1cncf  20322  cncfmet  20325  evth2  20373  lmmbr2  20611  lmmbrf  20614  iscfil2  20618  cfil3i  20621  iscau2  20629  iscau4  20631  iscauf  20632  caucfil  20635  iscmet3lem3  20642  cfilres  20648  causs  20650  lmclim  20654  rrxmet  20748  evthicc2  20785  cniccbdd  20786  ovolfioo  20792  ovolficc  20793  ismbl2  20851  mbfsup  20983  mbfinf  20984  mbflimsup  20985  0plef  20991  mbfi1flim  21042  xrge0f  21050  itg2mulclem  21065  itgeqa  21132  ellimc2  21193  ellimc3  21195  limcflf  21197  cnlimc  21204  dvferm1  21298  dvferm2  21300  rolle  21303  dvivthlem1  21321  ftc1lem6  21354  itgsubst  21362  mdegle0  21432  deg1leb  21450  plydivex  21647  ulm2  21734  ulmcaulem  21743  ulmcau  21744  ulmdvlem3  21751  abelthlem9  21789  abelth  21790  rlimcnp  22243  ftalem3  22296  issqf  22358  sqf11  22361  dvdsmulf1o  22418  dchrelbas4  22466  dchrinv  22484  2sqlem6  22592  chpo1ubb  22614  dchrmusumlema  22626  dchrisum0lema  22647  ostth3  22771  eqeelen  22972  brbtwn2  22973  colinearalg  22978  axcgrid  22984  axsegconlem1  22985  ax5seglem4  23000  ax5seglem5  23001  axbtwnid  23007  axpasch  23009  axeuclidlem  23030  axcontlem2  23033  axcontlem4  23035  axcontlem7  23038  axcontlem12  23043  isgrpo2  23506  nmounbi  23998  blocnilem  24026  isph  24044  phoeqi  24080  h2hcau  24203  h2hlm  24204  hial2eq2  24331  hoeq1  25056  hoeq2  25057  adjsym  25059  cnvadj  25118  hhcno  25130  hhcnf  25131  adjvalval  25163  leop2  25350  leoptri  25362  mdbr2  25522  dmdbr2  25529  mddmd2  25535  cdj3lem3b  25666  fcnvgreu  25814  toslublem  25950  tosglblem  25952  submarchi  26026  isarchi3  26027  lmdvg  26236  eulerpartlemd  26596  subfacp1lem3  26917  subfacp1lem5  26919  dfrdg2  27455  itg2gt0cn  28288  ftc1cnnc  28307  opnrebl  28356  lmclim2  28495  caures  28497  sstotbnd2  28514  rrnmet  28569  rrncmslem  28572  isdrngo3  28606  isidlc  28656  wepwsolem  29236  fnwe2lem2  29246  islnm2  29273  caofcan  29439  wwlknext  30199  clwwlkel  30298  clwwlkf  30299  wwlkext2clwwlk  30308  wwlksubclwwlk  30309  clwlkfclwwlk  30360  extwwlkfablem2  30514  numclwwlkovf2ex  30522  islinindfis  30689  cvrval2  32489  isat3  32522  iscvlat2N  32539  glbconN  32591  ltrneq  33363  cdlemefrs29clN  33613  cdlemefrs32fva  33614  cdleme32fva  33651  cdlemk33N  34123  cdlemk34  34124  cdlemkid3N  34147  cdlemkid4  34148  diaglbN  34270  dibglbN  34381  dihglbcpreN  34515  dihglblem6  34555  hdmap1eulem  35039  hdmap1eulemOLDN  35040  hdmapoc  35149  hlhilocv  35175
  Copyright terms: Public domain W3C validator