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

Theorem ralbidva 2559
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 1605 . 2  |-  F/ x ph
2 ralbidva.1 . 2  |-  ( (
ph  /\  x  e.  A )  ->  ( ps 
<->  ch ) )
31, 2ralbida 2557 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 1684   A.wral 2543
This theorem is referenced by:  raleqbidva  2750  ordunisssuc  4495  tfindsg2  4652  poinxp  4753  soinxp  4754  frinxp  4755  funimass3  5641  fnsuppres  5732  cocan1  5801  cocan2  5802  isores2  5830  isoini2  5836  f1oweALT  5851  ofrfval  6086  ofrfval2  6096  dfsmo2  6364  smores  6369  smores2  6371  ac6sfi  7101  fimaxg  7104  ordunifi  7107  isfinite2  7115  fipreima  7161  supisolem  7221  ordiso2  7230  ordtypelem7  7239  cantnf  7395  wemapwe  7400  rankval3b  7498  rankonidlem  7500  iscard  7608  acndom  7678  dfac12lem3  7771  kmlem2  7777  cflim2  7889  cfsmolem  7896  ttukeylem6  8141  alephreg  8204  suplem2pr  8677  axsup  8898  sup3  9711  infm3  9713  suprleub  9718  dfinfmr  9731  infmrgelb  9734  ofsubeq0  9743  ofsubge0  9745  zextlt  10086  prime  10092  indstr  10287  supxr2  10632  supxrbnd1  10640  supxrbnd2  10641  supxrleub  10645  supxrbnd  10647  infmxrgelb  10653  fzshftral  10869  clim  11968  rlim  11969  clim2  11978  clim2c  11979  clim0c  11981  ello1mpt  11995  lo1o1  12006  o1lo1  12011  climabs0  12059  o1compt  12061  rlimdiv  12119  geomulcvg  12332  mertenslem2  12341  mertens  12342  rpnnen2  12504  sqr2irr  12527  pc11  12932  pcz  12933  1arith  12974  vdwlem8  13035  vdwlem11  13038  vdw  13041  ramval  13055  pwsle  13391  mrieqvd  13540  mreacs  13560  cidpropd  13613  ismon2  13637  monpropd  13640  isepi  13643  isepi2  13644  subsubc  13727  funcres2b  13771  funcpropd  13774  isfull2  13785  isfth2  13789  fucsect  13846  fucinv  13847  pospropd  14238  ipodrsfi  14266  tsrss  14332  mndpropd  14398  grpidpropd  14399  grppropd  14500  issubg4  14638  gass  14755  gexdvds  14895  gexdvds2  14896  subgpgp  14908  sylow3lem6  14943  efgval2  15033  efgsp1  15046  dprdf11  15258  subgdmdprd  15269  rngpropd  15372  abvpropd  15607  lsspropd  15774  lbspropd  15852  assapropd  16067  psrbaglefi  16118  psrbagconf1o  16120  gsumbagdiaglem  16121  mplmonmul  16208  phlpropd  16559  ishil2  16619  tgss2  16725  isclo  16824  neips  16850  opnnei  16857  isperf3  16884  ssidcn  16985  lmbrf  16990  cnrest2  17014  lmss  17026  lmres  17028  ist1-2  17075  ist1-3  17077  isreg2  17105  cmpfi  17135  1stccn  17189  subislly  17207  kgencn  17251  ptclsg  17309  ptcnplem  17315  xkococnlem  17353  xkoinjcn  17381  tgqtop  17403  qtopcn  17405  fbflim  17671  flimrest  17678  flfnei  17686  isflf  17688  cnflf  17697  fclsopn  17709  fclsbas  17716  fclsrest  17719  isfcf  17729  cnfcf  17737  ptcmplem3  17748  tmdgsum2  17779  eltsms  17815  tsmsgsum  17821  tsmssubm  17825  tsmsf1o  17827  ismet2  17898  prdsxmetlem  17932  elmopn2  17991  prdsbl  18037  metss  18054  metrest  18070  metcnp  18087  metcnp2  18088  metcn  18089  nrginvrcn  18202  metdsge  18353  divcn  18372  elcncf2  18394  mulc1cncf  18409  cncfmet  18412  evth2  18458  lmmbr2  18685  lmmbrf  18688  iscfil2  18692  cfil3i  18695  iscau2  18703  iscau4  18705  iscauf  18706  caucfil  18709  iscmet3lem3  18716  cfilres  18722  causs  18724  lmclim  18728  evthicc2  18820  cniccbdd  18821  ovolfioo  18827  ovolficc  18828  ismbl2  18886  mbfsup  19019  mbfinf  19020  mbflimsup  19021  0plef  19027  mbfi1flim  19078  xrge0f  19086  itg2mulclem  19101  itgeqa  19168  ellimc2  19227  ellimc3  19229  limcflf  19231  cnlimc  19238  dvferm1  19332  dvferm2  19334  rolle  19337  dvivthlem1  19355  ftc1lem6  19388  itgsubst  19396  mdegle0  19463  deg1leb  19481  plydivex  19677  ulm2  19764  ulmcaulem  19771  ulmcau  19772  ulmdvlem3  19779  abelthlem9  19816  abelth  19817  rlimcnp  20260  ftalem3  20312  issqf  20374  sqf11  20377  dvdsmulf1o  20434  dchrelbas4  20482  dchrinv  20500  2sqlem6  20608  chpo1ubb  20630  dchrmusumlema  20642  dchrisum0lema  20663  ostth3  20787  isgrpo2  20864  nmounbi  21354  blocnilem  21382  isph  21400  phoeqi  21436  h2hcau  21559  h2hlm  21560  hial2eq2  21686  hoeq1  22410  hoeq2  22411  adjsym  22413  cnvadj  22472  hhcno  22484  hhcnf  22485  adjvalval  22517  leop2  22704  leoptri  22716  mdbr2  22876  dmdbr2  22883  mddmd2  22889  cdj3lem3b  23020  lmdvg  23376  subfacp1lem3  23713  subfacp1lem5  23715  dfrdg2  24152  tfrALTlem  24276  eqeelen  24532  brbtwn2  24533  colinearalg  24538  axcgrid  24544  axsegconlem1  24545  ax5seglem4  24560  ax5seglem5  24561  axbtwnid  24567  axpasch  24569  axeuclidlem  24590  axcontlem2  24593  axcontlem4  24595  axcontlem7  24598  axcontlem12  24603  surjsec2  25120  prl2  25169  idlvalNEW  25445  istopxc  25548  lvsovso2  25627  supnuf  25629  supexr  25631  tcnvec  25690  opnrebl  26235  lmclim2  26474  caures  26476  sstotbnd2  26498  rrnmet  26553  rrncmslem  26556  isdrngo3  26590  isidlc  26640  fnnfpeq0  26758  wepwsolem  27138  fnwe2lem2  27148  islnm2  27176  lindfmm  27297  islindf4  27308  islindf5  27309  caofcan  27540  cvrval2  29464  isat3  29497  iscvlat2N  29514  glbconN  29566  ltrneq  30338  cdlemefrs29clN  30588  cdlemefrs32fva  30589  cdleme32fva  30626  cdlemk33N  31098  cdlemk34  31099  cdlemkid3N  31122  cdlemkid4  31123  diaglbN  31245  dibglbN  31356  dihglbcpreN  31490  dihglblem6  31530  hdmap1eulem  32014  hdmap1eulemOLDN  32015  hdmapoc  32124  hlhilocv  32150
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-11 1715
This theorem depends on definitions:  df-bi 177  df-an 360  df-nf 1532  df-ral 2548
  Copyright terms: Public domain W3C validator