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

Theorem ralbidva 2752
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 1673 . 2  |-  F/ x ph
2 ralbidva.1 . 2  |-  ( (
ph  /\  x  e.  A )  ->  ( ps 
<->  ch ) )
31, 2ralbida 2750 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 1756   A.wral 2736
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-12 1792
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1587  df-nf 1590  df-ral 2741
This theorem is referenced by:  raleqbidva  2954  ordunisssuc  4842  poinxp  4923  soinxp  4924  frinxp  4925  fnmptfvd  5827  funimass3  5840  fnnfpeq0  5930  fnsuppresOLD  5959  cocan1  6016  cocan2  6017  isores2  6045  isoini2  6051  ofrfval  6349  ofrfval2  6358  tfindsg2  6493  f1oweALT  6582  fnsuppres  6737  dfsmo2  6829  smores  6834  smores2  6836  ac6sfi  7577  fimaxg  7580  ordunifi  7583  isfinite2  7591  fipreima  7638  supisolem  7741  ordiso2  7750  ordtypelem7  7759  cantnf  7922  cantnfOLD  7944  wemapwe  7949  wemapweOLD  7950  rankval3b  8054  rankonidlem  8056  iscard  8166  acndom  8242  dfac12lem3  8335  kmlem2  8341  cflim2  8453  cfsmolem  8460  ttukeylem6  8704  alephreg  8767  suplem2pr  9243  axsup  9471  sup3  10308  infm3  10310  suprleub  10315  dfinfmr  10328  infmrgelb  10331  ofsubeq0  10340  ofsubge0  10342  zextlt  10737  prime  10743  indstr  10944  supxr2  11297  supxrbnd1  11305  supxrbnd2  11306  supxrleub  11310  supxrbnd  11312  infmxrgelb  11318  fzshftral  11568  swrdeq  12361  swrdsymbeq  12362  clim  12993  rlim  12994  clim2  13003  clim2c  13004  clim0c  13006  ello1mpt  13020  lo1o1  13031  o1lo1  13036  climabs0  13084  o1compt  13086  rlimdiv  13144  geomulcvg  13357  mertenslem2  13366  mertens  13367  rpnnen2  13529  sqr2irr  13552  pc11  13967  pcz  13968  1arith  14009  vdwlem8  14070  vdwlem11  14073  vdw  14076  ramval  14090  pwsle  14451  mrieqvd  14597  mreacs  14617  cidpropd  14670  ismon2  14694  monpropd  14697  isepi  14700  isepi2  14701  subsubc  14784  funcres2b  14828  funcpropd  14831  isfull2  14842  isfth2  14846  fucsect  14903  fucinv  14904  pospropd  15325  ipodrsfi  15354  tsrss  15414  mndpropd  15467  grpidpropd  15468  grppropd  15577  issubg4  15721  gass  15840  gsmsymgrfixlem1  15953  gsmsymgreqlem2  15957  gexdvds  16104  gexdvds2  16105  subgpgp  16117  sylow3lem6  16152  efgval2  16242  efgsp1  16255  dprdf11  16535  dprdf11OLD  16542  subgdmdprd  16553  rngpropd  16698  abvpropd  16949  lsspropd  17120  lbspropd  17202  assapropd  17420  psrbaglefi  17463  psrbaglefiOLD  17464  psrbagconf1o  17466  gsumbagdiaglem  17467  mplmonmul  17565  phlpropd  18106  ishil2  18166  lindfmm  18278  islindf4  18289  islindf5  18290  tgss2  18614  isclo  18713  neips  18739  opnnei  18746  isperf3  18779  ssidcn  18881  lmbrf  18886  cnnei  18908  cnrest2  18912  lmss  18924  lmres  18926  ist1-2  18973  ist1-3  18975  isreg2  19003  cmpfi  19033  bwth  19035  1stccn  19089  subislly  19107  kgencn  19151  ptclsg  19210  ptcnplem  19216  xkococnlem  19254  xkoinjcn  19282  tgqtop  19307  qtopcn  19309  fbflim  19571  flimrest  19578  flfnei  19586  isflf  19588  cnflf  19597  fclsopn  19609  fclsbas  19616  fclsrest  19619  isfcf  19629  cnfcf  19637  ptcmplem3  19648  tmdgsum2  19689  eltsms  19725  tsmsgsum  19731  tsmsgsumOLD  19734  tsmssubm  19738  tsmsf1o  19741  utopsnneiplem  19844  ismet2  19930  prdsxmetlem  19965  elmopn2  20042  prdsbl  20088  metss  20105  metrest  20121  metcnp  20138  metcnp2  20139  metcn  20140  metucnOLD  20185  metucn  20186  nrginvrcn  20294  metdsge  20447  divcn  20466  elcncf2  20488  mulc1cncf  20503  cncfmet  20506  evth2  20554  lmmbr2  20792  lmmbrf  20795  iscfil2  20799  cfil3i  20802  iscau2  20810  iscau4  20812  iscauf  20813  caucfil  20816  iscmet3lem3  20823  cfilres  20829  causs  20831  lmclim  20835  rrxmet  20929  evthicc2  20966  cniccbdd  20967  ovolfioo  20973  ovolficc  20974  ismbl2  21032  mbfsup  21164  mbfinf  21165  mbflimsup  21166  0plef  21172  mbfi1flim  21223  xrge0f  21231  itg2mulclem  21246  itgeqa  21313  ellimc2  21374  ellimc3  21376  limcflf  21378  cnlimc  21385  dvferm1  21479  dvferm2  21481  rolle  21484  dvivthlem1  21502  ftc1lem6  21535  itgsubst  21543  mdegle0  21570  deg1leb  21588  plydivex  21785  ulm2  21872  ulmcaulem  21881  ulmcau  21882  ulmdvlem3  21889  abelthlem9  21927  abelth  21928  rlimcnp  22381  ftalem3  22434  issqf  22496  sqf11  22499  dvdsmulf1o  22556  dchrelbas4  22604  dchrinv  22622  2sqlem6  22730  chpo1ubb  22752  dchrmusumlema  22764  dchrisum0lema  22785  ostth3  22909  eqeelen  23172  brbtwn2  23173  colinearalg  23178  axcgrid  23184  axsegconlem1  23185  ax5seglem4  23200  ax5seglem5  23201  axbtwnid  23207  axpasch  23209  axeuclidlem  23230  axcontlem2  23233  axcontlem4  23235  axcontlem7  23238  axcontlem12  23243  isgrpo2  23706  nmounbi  24198  blocnilem  24226  isph  24244  phoeqi  24280  h2hcau  24403  h2hlm  24404  hial2eq2  24531  hoeq1  25256  hoeq2  25257  adjsym  25259  cnvadj  25318  hhcno  25330  hhcnf  25331  adjvalval  25363  leop2  25550  leoptri  25562  mdbr2  25722  dmdbr2  25729  mddmd2  25735  cdj3lem3b  25866  fcnvgreu  26013  toslublem  26150  tosglblem  26152  submarchi  26225  isarchi3  26226  lmdvg  26405  eulerpartlemd  26771  subfacp1lem3  27092  subfacp1lem5  27094  dfrdg2  27631  itg2gt0cn  28473  ftc1cnnc  28492  opnrebl  28541  lmclim2  28680  caures  28682  sstotbnd2  28699  rrnmet  28754  rrncmslem  28757  isdrngo3  28791  isidlc  28841  wepwsolem  29420  fnwe2lem2  29430  islnm2  29457  caofcan  29623  wwlknext  30382  clwwlkel  30481  clwwlkf  30482  wwlkext2clwwlk  30491  wwlksubclwwlk  30492  clwlkfclwwlk  30543  extwwlkfablem2  30697  numclwwlkovf2ex  30705  suprfinzcl  30774  mptnn0fsupp  30832  scmatsubcl  30923  islinindfis  30980  cnstpmatel2  31065  1elcnstpmat  31067  cnstpmatmcllem  31070  cnstpmatmcl  31071  m2pminv2  31101  pmatcollpw2lem  31120  pmattomply1lem  31123  pmattomply1mhmlem0  31142  pmattomply1mhmlem1  31143  cvrval2  33015  isat3  33048  iscvlat2N  33065  glbconN  33117  ltrneq  33889  cdlemefrs29clN  34139  cdlemefrs32fva  34140  cdleme32fva  34177  cdlemk33N  34649  cdlemk34  34650  cdlemkid3N  34673  cdlemkid4  34674  diaglbN  34796  dibglbN  34907  dihglbcpreN  35041  dihglblem6  35081  hdmap1eulem  35565  hdmap1eulemOLDN  35566  hdmapoc  35675  hlhilocv  35701
  Copyright terms: Public domain W3C validator