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

Theorem ralbidva 2572
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 1609 . 2  |-  F/ x ph
2 ralbidva.1 . 2  |-  ( (
ph  /\  x  e.  A )  ->  ( ps 
<->  ch ) )
31, 2ralbida 2570 1  |-  ( ph  ->  ( A. x  e.  A  ps  <->  A. x  e.  A  ch )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    /\ wa 358    e. wcel 1696   A.wral 2556
This theorem is referenced by:  raleqbidva  2763  ordunisssuc  4511  tfindsg2  4668  poinxp  4769  soinxp  4770  frinxp  4771  funimass3  5657  fnsuppres  5748  cocan1  5817  cocan2  5818  isores2  5846  isoini2  5852  f1oweALT  5867  ofrfval  6102  ofrfval2  6112  dfsmo2  6380  smores  6385  smores2  6387  ac6sfi  7117  fimaxg  7120  ordunifi  7123  isfinite2  7131  fipreima  7177  supisolem  7237  ordiso2  7246  ordtypelem7  7255  cantnf  7411  wemapwe  7416  rankval3b  7514  rankonidlem  7516  iscard  7624  acndom  7694  dfac12lem3  7787  kmlem2  7793  cflim2  7905  cfsmolem  7912  ttukeylem6  8157  alephreg  8220  suplem2pr  8693  axsup  8914  sup3  9727  infm3  9729  suprleub  9734  dfinfmr  9747  infmrgelb  9750  ofsubeq0  9759  ofsubge0  9761  zextlt  10102  prime  10108  indstr  10303  supxr2  10648  supxrbnd1  10656  supxrbnd2  10657  supxrleub  10661  supxrbnd  10663  infmxrgelb  10669  fzshftral  10885  clim  11984  rlim  11985  clim2  11994  clim2c  11995  clim0c  11997  ello1mpt  12011  lo1o1  12022  o1lo1  12027  climabs0  12075  o1compt  12077  rlimdiv  12135  geomulcvg  12348  mertenslem2  12357  mertens  12358  rpnnen2  12520  sqr2irr  12543  pc11  12948  pcz  12949  1arith  12990  vdwlem8  13051  vdwlem11  13054  vdw  13057  ramval  13071  pwsle  13407  mrieqvd  13556  mreacs  13576  cidpropd  13629  ismon2  13653  monpropd  13656  isepi  13659  isepi2  13660  subsubc  13743  funcres2b  13787  funcpropd  13790  isfull2  13801  isfth2  13805  fucsect  13862  fucinv  13863  pospropd  14254  ipodrsfi  14282  tsrss  14348  mndpropd  14414  grpidpropd  14415  grppropd  14516  issubg4  14654  gass  14771  gexdvds  14911  gexdvds2  14912  subgpgp  14924  sylow3lem6  14959  efgval2  15049  efgsp1  15062  dprdf11  15274  subgdmdprd  15285  rngpropd  15388  abvpropd  15623  lsspropd  15790  lbspropd  15868  assapropd  16083  psrbaglefi  16134  psrbagconf1o  16136  gsumbagdiaglem  16137  mplmonmul  16224  phlpropd  16575  ishil2  16635  tgss2  16741  isclo  16840  neips  16866  opnnei  16873  isperf3  16900  ssidcn  17001  lmbrf  17006  cnrest2  17030  lmss  17042  lmres  17044  ist1-2  17091  ist1-3  17093  isreg2  17121  cmpfi  17151  1stccn  17205  subislly  17223  kgencn  17267  ptclsg  17325  ptcnplem  17331  xkococnlem  17369  xkoinjcn  17397  tgqtop  17419  qtopcn  17421  fbflim  17687  flimrest  17694  flfnei  17702  isflf  17704  cnflf  17713  fclsopn  17725  fclsbas  17732  fclsrest  17735  isfcf  17745  cnfcf  17753  ptcmplem3  17764  tmdgsum2  17795  eltsms  17831  tsmsgsum  17837  tsmssubm  17841  tsmsf1o  17843  ismet2  17914  prdsxmetlem  17948  elmopn2  18007  prdsbl  18053  metss  18070  metrest  18086  metcnp  18103  metcnp2  18104  metcn  18105  nrginvrcn  18218  metdsge  18369  divcn  18388  elcncf2  18410  mulc1cncf  18425  cncfmet  18428  evth2  18474  lmmbr2  18701  lmmbrf  18704  iscfil2  18708  cfil3i  18711  iscau2  18719  iscau4  18721  iscauf  18722  caucfil  18725  iscmet3lem3  18732  cfilres  18738  causs  18740  lmclim  18744  evthicc2  18836  cniccbdd  18837  ovolfioo  18843  ovolficc  18844  ismbl2  18902  mbfsup  19035  mbfinf  19036  mbflimsup  19037  0plef  19043  mbfi1flim  19094  xrge0f  19102  itg2mulclem  19117  itgeqa  19184  ellimc2  19243  ellimc3  19245  limcflf  19247  cnlimc  19254  dvferm1  19348  dvferm2  19350  rolle  19353  dvivthlem1  19371  ftc1lem6  19404  itgsubst  19412  mdegle0  19479  deg1leb  19497  plydivex  19693  ulm2  19780  ulmcaulem  19787  ulmcau  19788  ulmdvlem3  19795  abelthlem9  19832  abelth  19833  rlimcnp  20276  ftalem3  20328  issqf  20390  sqf11  20393  dvdsmulf1o  20450  dchrelbas4  20498  dchrinv  20516  2sqlem6  20624  chpo1ubb  20646  dchrmusumlema  20658  dchrisum0lema  20679  ostth3  20803  isgrpo2  20880  nmounbi  21370  blocnilem  21398  isph  21416  phoeqi  21452  h2hcau  21575  h2hlm  21576  hial2eq2  21702  hoeq1  22426  hoeq2  22427  adjsym  22429  cnvadj  22488  hhcno  22500  hhcnf  22501  adjvalval  22533  leop2  22720  leoptri  22732  mdbr2  22892  dmdbr2  22899  mddmd2  22905  cdj3lem3b  23036  lmdvg  23391  subfacp1lem3  23728  subfacp1lem5  23730  dfrdg2  24223  tfrALTlem  24347  eqeelen  24604  brbtwn2  24605  colinearalg  24610  axcgrid  24616  axsegconlem1  24617  ax5seglem4  24632  ax5seglem5  24633  axbtwnid  24639  axpasch  24641  axeuclidlem  24662  axcontlem2  24665  axcontlem4  24667  axcontlem7  24670  axcontlem12  24675  itg2gt0cn  25006  ftc1cnnc  25025  surjsec2  25223  prl2  25272  idlvalNEW  25548  istopxc  25651  lvsovso2  25730  supnuf  25732  supexr  25734  tcnvec  25793  opnrebl  26338  lmclim2  26577  caures  26579  sstotbnd2  26601  rrnmet  26656  rrncmslem  26659  isdrngo3  26693  isidlc  26743  fnnfpeq0  26861  wepwsolem  27241  fnwe2lem2  27251  islnm2  27279  lindfmm  27400  islindf4  27411  islindf5  27412  caofcan  27643  cvrval2  30086  isat3  30119  iscvlat2N  30136  glbconN  30188  ltrneq  30960  cdlemefrs29clN  31210  cdlemefrs32fva  31211  cdleme32fva  31248  cdlemk33N  31720  cdlemk34  31721  cdlemkid3N  31744  cdlemkid4  31745  diaglbN  31867  dibglbN  31978  dihglbcpreN  32112  dihglblem6  32152  hdmap1eulem  32636  hdmap1eulemOLDN  32637  hdmapoc  32746  hlhilocv  32772
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-nf 1535  df-ral 2561
  Copyright terms: Public domain W3C validator