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

Theorem ralbidva 2713
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 1629 . 2  |-  F/ x ph
2 ralbidva.1 . 2  |-  ( (
ph  /\  x  e.  A )  ->  ( ps 
<->  ch ) )
31, 2ralbida 2711 1  |-  ( ph  ->  ( A. x  e.  A  ps  <->  A. x  e.  A  ch )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    /\ wa 359    e. wcel 1725   A.wral 2697
This theorem is referenced by:  raleqbidva  2910  ordunisssuc  4676  tfindsg2  4833  poinxp  4933  soinxp  4934  frinxp  4935  funimass3  5838  fnsuppres  5944  cocan1  6016  cocan2  6017  isores2  6045  isoini2  6051  f1oweALT  6066  ofrfval  6305  ofrfval2  6315  dfsmo2  6601  smores  6606  smores2  6608  ac6sfi  7343  fimaxg  7346  ordunifi  7349  isfinite2  7357  fipreima  7404  supisolem  7467  ordiso2  7476  ordtypelem7  7485  cantnf  7641  wemapwe  7646  rankval3b  7744  rankonidlem  7746  iscard  7854  acndom  7924  dfac12lem3  8017  kmlem2  8023  cflim2  8135  cfsmolem  8142  ttukeylem6  8386  alephreg  8449  suplem2pr  8922  axsup  9143  sup3  9957  infm3  9959  suprleub  9964  dfinfmr  9977  infmrgelb  9980  ofsubeq0  9989  ofsubge0  9991  zextlt  10336  prime  10342  indstr  10537  supxr2  10884  supxrbnd1  10892  supxrbnd2  10893  supxrleub  10897  supxrbnd  10899  infmxrgelb  10905  fzshftral  11126  clim  12280  rlim  12281  clim2  12290  clim2c  12291  clim0c  12293  ello1mpt  12307  lo1o1  12318  o1lo1  12323  climabs0  12371  o1compt  12373  rlimdiv  12431  geomulcvg  12645  mertenslem2  12654  mertens  12655  rpnnen2  12817  sqr2irr  12840  pc11  13245  pcz  13246  1arith  13287  vdwlem8  13348  vdwlem11  13351  vdw  13354  ramval  13368  pwsle  13706  mrieqvd  13855  mreacs  13875  cidpropd  13928  ismon2  13952  monpropd  13955  isepi  13958  isepi2  13959  subsubc  14042  funcres2b  14086  funcpropd  14089  isfull2  14100  isfth2  14104  fucsect  14161  fucinv  14162  pospropd  14553  ipodrsfi  14581  tsrss  14647  mndpropd  14713  grpidpropd  14714  grppropd  14815  issubg4  14953  gass  15070  gexdvds  15210  gexdvds2  15211  subgpgp  15223  sylow3lem6  15258  efgval2  15348  efgsp1  15361  dprdf11  15573  subgdmdprd  15584  rngpropd  15687  abvpropd  15922  lsspropd  16085  lbspropd  16163  assapropd  16378  psrbaglefi  16429  psrbagconf1o  16431  gsumbagdiaglem  16432  mplmonmul  16519  phlpropd  16878  ishil2  16938  tgss2  17044  isclo  17143  neips  17169  opnnei  17176  isperf3  17209  ssidcn  17311  lmbrf  17316  cnnei  17338  cnrest2  17342  lmss  17354  lmres  17356  ist1-2  17403  ist1-3  17405  isreg2  17433  cmpfi  17463  1stccn  17518  subislly  17536  kgencn  17580  ptclsg  17639  ptcnplem  17645  xkococnlem  17683  xkoinjcn  17711  tgqtop  17736  qtopcn  17738  fbflim  18000  flimrest  18007  flfnei  18015  isflf  18017  cnflf  18026  fclsopn  18038  fclsbas  18045  fclsrest  18048  isfcf  18058  cnfcf  18066  ptcmplem3  18077  tmdgsum2  18118  eltsms  18154  tsmsgsum  18160  tsmssubm  18164  tsmsf1o  18166  utopsnneiplem  18269  ismet2  18355  prdsxmetlem  18390  elmopn2  18467  prdsbl  18513  metss  18530  metrest  18546  metcnp  18563  metcnp2  18564  metcn  18565  metucnOLD  18610  metucn  18611  nrginvrcn  18719  metdsge  18871  divcn  18890  elcncf2  18912  mulc1cncf  18927  cncfmet  18930  evth2  18977  lmmbr2  19204  lmmbrf  19207  iscfil2  19211  cfil3i  19214  iscau2  19222  iscau4  19224  iscauf  19225  caucfil  19228  iscmet3lem3  19235  cfilres  19241  causs  19243  lmclim  19247  evthicc2  19349  cniccbdd  19350  ovolfioo  19356  ovolficc  19357  ismbl2  19415  mbfsup  19548  mbfinf  19549  mbflimsup  19550  0plef  19556  mbfi1flim  19607  xrge0f  19615  itg2mulclem  19630  itgeqa  19697  ellimc2  19756  ellimc3  19758  limcflf  19760  cnlimc  19767  dvferm1  19861  dvferm2  19863  rolle  19866  dvivthlem1  19884  ftc1lem6  19917  itgsubst  19925  mdegle0  19992  deg1leb  20010  plydivex  20206  ulm2  20293  ulmcaulem  20302  ulmcau  20303  ulmdvlem3  20310  abelthlem9  20348  abelth  20349  rlimcnp  20796  ftalem3  20849  issqf  20911  sqf11  20914  dvdsmulf1o  20971  dchrelbas4  21019  dchrinv  21037  2sqlem6  21145  chpo1ubb  21167  dchrmusumlema  21179  dchrisum0lema  21200  ostth3  21324  isgrpo2  21777  nmounbi  22269  blocnilem  22297  isph  22315  phoeqi  22351  h2hcau  22474  h2hlm  22475  hial2eq2  22601  hoeq1  23325  hoeq2  23326  adjsym  23328  cnvadj  23387  hhcno  23399  hhcnf  23400  adjvalval  23432  leop2  23619  leoptri  23631  mdbr2  23791  dmdbr2  23798  mddmd2  23804  cdj3lem3b  23935  toslub  24183  tosglb  24184  lmdvg  24330  subfacp1lem3  24860  subfacp1lem5  24862  dfrdg2  25415  eqeelen  25835  brbtwn2  25836  colinearalg  25841  axcgrid  25847  axsegconlem1  25848  ax5seglem4  25863  ax5seglem5  25864  axbtwnid  25870  axpasch  25872  axeuclidlem  25893  axcontlem2  25896  axcontlem4  25898  axcontlem7  25901  axcontlem12  25906  itg2gt0cn  26250  ftc1cnnc  26269  opnrebl  26314  lmclim2  26455  caures  26457  sstotbnd2  26474  rrnmet  26529  rrncmslem  26532  isdrngo3  26566  isidlc  26616  fnnfpeq0  26730  wepwsolem  27107  fnwe2lem2  27117  islnm2  27144  lindfmm  27265  islindf4  27276  islindf5  27277  caofcan  27508  cvrval2  30009  isat3  30042  iscvlat2N  30059  glbconN  30111  ltrneq  30883  cdlemefrs29clN  31133  cdlemefrs32fva  31134  cdleme32fva  31171  cdlemk33N  31643  cdlemk34  31644  cdlemkid3N  31667  cdlemkid4  31668  diaglbN  31790  dibglbN  31901  dihglbcpreN  32035  dihglblem6  32075  hdmap1eulem  32559  hdmap1eulemOLDN  32560  hdmapoc  32669  hlhilocv  32695
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-ral 2702
  Copyright terms: Public domain W3C validator