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

Theorem ralbidva 2682
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 1626 . 2  |-  F/ x ph
2 ralbidva.1 . 2  |-  ( (
ph  /\  x  e.  A )  ->  ( ps 
<->  ch ) )
31, 2ralbida 2680 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 1721   A.wral 2666
This theorem is referenced by:  raleqbidva  2878  ordunisssuc  4643  tfindsg2  4800  poinxp  4900  soinxp  4901  frinxp  4902  funimass3  5805  fnsuppres  5911  cocan1  5983  cocan2  5984  isores2  6012  isoini2  6018  f1oweALT  6033  ofrfval  6272  ofrfval2  6282  dfsmo2  6568  smores  6573  smores2  6575  ac6sfi  7310  fimaxg  7313  ordunifi  7316  isfinite2  7324  fipreima  7370  supisolem  7431  ordiso2  7440  ordtypelem7  7449  cantnf  7605  wemapwe  7610  rankval3b  7708  rankonidlem  7710  iscard  7818  acndom  7888  dfac12lem3  7981  kmlem2  7987  cflim2  8099  cfsmolem  8106  ttukeylem6  8350  alephreg  8413  suplem2pr  8886  axsup  9107  sup3  9921  infm3  9923  suprleub  9928  dfinfmr  9941  infmrgelb  9944  ofsubeq0  9953  ofsubge0  9955  zextlt  10300  prime  10306  indstr  10501  supxr2  10848  supxrbnd1  10856  supxrbnd2  10857  supxrleub  10861  supxrbnd  10863  infmxrgelb  10869  fzshftral  11089  clim  12243  rlim  12244  clim2  12253  clim2c  12254  clim0c  12256  ello1mpt  12270  lo1o1  12281  o1lo1  12286  climabs0  12334  o1compt  12336  rlimdiv  12394  geomulcvg  12608  mertenslem2  12617  mertens  12618  rpnnen2  12780  sqr2irr  12803  pc11  13208  pcz  13209  1arith  13250  vdwlem8  13311  vdwlem11  13314  vdw  13317  ramval  13331  pwsle  13669  mrieqvd  13818  mreacs  13838  cidpropd  13891  ismon2  13915  monpropd  13918  isepi  13921  isepi2  13922  subsubc  14005  funcres2b  14049  funcpropd  14052  isfull2  14063  isfth2  14067  fucsect  14124  fucinv  14125  pospropd  14516  ipodrsfi  14544  tsrss  14610  mndpropd  14676  grpidpropd  14677  grppropd  14778  issubg4  14916  gass  15033  gexdvds  15173  gexdvds2  15174  subgpgp  15186  sylow3lem6  15221  efgval2  15311  efgsp1  15324  dprdf11  15536  subgdmdprd  15547  rngpropd  15650  abvpropd  15885  lsspropd  16048  lbspropd  16126  assapropd  16341  psrbaglefi  16392  psrbagconf1o  16394  gsumbagdiaglem  16395  mplmonmul  16482  phlpropd  16841  ishil2  16901  tgss2  17007  isclo  17106  neips  17132  opnnei  17139  isperf3  17171  ssidcn  17273  lmbrf  17278  cnnei  17300  cnrest2  17304  lmss  17316  lmres  17318  ist1-2  17365  ist1-3  17367  isreg2  17395  cmpfi  17425  1stccn  17479  subislly  17497  kgencn  17541  ptclsg  17600  ptcnplem  17606  xkococnlem  17644  xkoinjcn  17672  tgqtop  17697  qtopcn  17699  fbflim  17961  flimrest  17968  flfnei  17976  isflf  17978  cnflf  17987  fclsopn  17999  fclsbas  18006  fclsrest  18009  isfcf  18019  cnfcf  18027  ptcmplem3  18038  tmdgsum2  18079  eltsms  18115  tsmsgsum  18121  tsmssubm  18125  tsmsf1o  18127  utopsnneiplem  18230  ismet2  18316  prdsxmetlem  18351  elmopn2  18428  prdsbl  18474  metss  18491  metrest  18507  metcnp  18524  metcnp2  18525  metcn  18526  metucnOLD  18571  metucn  18572  nrginvrcn  18680  metdsge  18832  divcn  18851  elcncf2  18873  mulc1cncf  18888  cncfmet  18891  evth2  18938  lmmbr2  19165  lmmbrf  19168  iscfil2  19172  cfil3i  19175  iscau2  19183  iscau4  19185  iscauf  19186  caucfil  19189  iscmet3lem3  19196  cfilres  19202  causs  19204  lmclim  19208  evthicc2  19310  cniccbdd  19311  ovolfioo  19317  ovolficc  19318  ismbl2  19376  mbfsup  19509  mbfinf  19510  mbflimsup  19511  0plef  19517  mbfi1flim  19568  xrge0f  19576  itg2mulclem  19591  itgeqa  19658  ellimc2  19717  ellimc3  19719  limcflf  19721  cnlimc  19728  dvferm1  19822  dvferm2  19824  rolle  19827  dvivthlem1  19845  ftc1lem6  19878  itgsubst  19886  mdegle0  19953  deg1leb  19971  plydivex  20167  ulm2  20254  ulmcaulem  20263  ulmcau  20264  ulmdvlem3  20271  abelthlem9  20309  abelth  20310  rlimcnp  20757  ftalem3  20810  issqf  20872  sqf11  20875  dvdsmulf1o  20932  dchrelbas4  20980  dchrinv  20998  2sqlem6  21106  chpo1ubb  21128  dchrmusumlema  21140  dchrisum0lema  21161  ostth3  21285  isgrpo2  21738  nmounbi  22230  blocnilem  22258  isph  22276  phoeqi  22312  h2hcau  22435  h2hlm  22436  hial2eq2  22562  hoeq1  23286  hoeq2  23287  adjsym  23289  cnvadj  23348  hhcno  23360  hhcnf  23361  adjvalval  23393  leop2  23580  leoptri  23592  mdbr2  23752  dmdbr2  23759  mddmd2  23765  cdj3lem3b  23896  toslub  24144  tosglb  24145  lmdvg  24291  subfacp1lem3  24821  subfacp1lem5  24823  dfrdg2  25366  tfrALTlem  25490  eqeelen  25747  brbtwn2  25748  colinearalg  25753  axcgrid  25759  axsegconlem1  25760  ax5seglem4  25775  ax5seglem5  25776  axbtwnid  25782  axpasch  25784  axeuclidlem  25805  axcontlem2  25808  axcontlem4  25810  axcontlem7  25813  axcontlem12  25818  itg2gt0cn  26159  ftc1cnnc  26178  opnrebl  26213  lmclim2  26354  caures  26356  sstotbnd2  26373  rrnmet  26428  rrncmslem  26431  isdrngo3  26465  isidlc  26515  fnnfpeq0  26629  wepwsolem  27006  fnwe2lem2  27016  islnm2  27044  lindfmm  27165  islindf4  27176  islindf5  27177  caofcan  27408  cvrval2  29757  isat3  29790  iscvlat2N  29807  glbconN  29859  ltrneq  30631  cdlemefrs29clN  30881  cdlemefrs32fva  30882  cdleme32fva  30919  cdlemk33N  31391  cdlemk34  31392  cdlemkid3N  31415  cdlemkid4  31416  diaglbN  31538  dibglbN  31649  dihglbcpreN  31783  dihglblem6  31823  hdmap1eulem  32307  hdmap1eulemOLDN  32308  hdmapoc  32417  hlhilocv  32443
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-11 1757
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1548  df-nf 1551  df-ral 2671
  Copyright terms: Public domain W3C validator