MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  rgen2 Structured version   Visualization version   GIF version

Theorem rgen2 3195
Description: Generalization rule for restricted quantification, with two quantifiers. This theorem should be used in place of rgen2a 3347 since it depends on a smaller set of axioms. (Contributed by NM, 30-May-1999.)
Hypothesis
Ref Expression
rgen2.1 ((𝑥𝐴𝑦𝐵) → 𝜑)
Assertion
Ref Expression
rgen2 𝑥𝐴𝑦𝐵 𝜑
Distinct variable groups:   𝑥,𝑦   𝑦,𝐴
Allowed substitution hints:   𝜑(𝑥,𝑦)   𝐴(𝑥)   𝐵(𝑥,𝑦)

Proof of Theorem rgen2
StepHypRef Expression
1 rgen2.1 . . 3 ((𝑥𝐴𝑦𝐵) → 𝜑)
21ralrimiva 3144 . 2 (𝑥𝐴 → ∀𝑦𝐵 𝜑)
32rgen 3067 1 𝑥𝐴𝑦𝐵 𝜑
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397  wcel 2107  wral 3065
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914
This theorem depends on definitions:  df-bi 206  df-an 398  df-ral 3066
This theorem is referenced by:  rgen3  3200  invdisjrabw  5095  invdisjrab  5096  sosn  5723  isoid  7279  f1owe  7303  epweon  7714  epweonALT  7715  f1stres  7950  f2ndres  7951  fnwelem  8068  soseq  8096  issmo  8299  oawordeulem  8506  naddf  8632  ecopover  8767  unfilem2  9262  dffi2  9366  inficl  9368  fipwuni  9369  fisn  9370  dffi3  9374  cantnfvalf  9608  r111  9718  alephf1  10028  alephiso  10041  dfac5lem4  10069  kmlem9  10101  ackbij1lem17  10179  fin1a2lem2  10344  fin1a2lem4  10346  axcc2lem  10379  smobeth  10529  nqereu  10872  addpqf  10887  mulpqf  10889  genpdm  10945  axaddf  11088  axmulf  11089  subf  11410  mulnzcnopr  11808  negiso  12142  cnref1o  12917  xaddf  13150  xmulf  13198  ioof  13371  om2uzf1oi  13865  om2uzisoi  13866  wrd2ind  14618  wwlktovf1  14853  reeff1  16009  divalglem9  16290  bitsf1  16333  smupf  16365  gcdf  16399  eucalgf  16466  qredeu  16541  1arith  16806  vdwapf  16851  xpsff1o  17456  catideu  17562  sscres  17713  fpwipodrs  18436  letsr  18489  mgmidmo  18522  frmdplusg  18671  efmndmgm  18702  smndex1mgm  18724  pwmnd  18754  mulgfval  18881  nmznsg  18977  efgmf  19502  efglem  19505  efgred  19537  isabli  19585  brric  20187  xrsmgm  20848  xrs1cmn  20853  xrge0subm  20854  xrsds  20856  cnsubmlem  20861  cnsubrglem  20863  nn0srg  20883  rge0srg  20884  rzgrp  21043  fibas  22343  fctop  22370  cctop  22372  iccordt  22581  txuni2  22932  fsubbas  23234  zfbas  23263  ismeti  23694  dscmet  23944  qtopbaslem  24138  tgqioo  24179  xrsxmet  24188  xrsdsre  24189  retopconn  24208  iccconn  24209  divcn  24247  abscncf  24280  recncf  24281  imcncf  24282  cjcncf  24283  iimulcn  24317  icopnfhmeo  24322  iccpnfhmeo  24324  xrhmeo  24325  cnllycmp  24335  bndth  24337  iundisj2  24929  dyadf  24971  reefiso  25823  recosf1o  25907  cxpcn3  26117  sgmf  26510  2lgslem1b  26756  lrcut  27254  addsf  27314  negscut  27359  negsf1o  27371  tgjustf  27457  ercgrg  27501  2wspmdisj  29323  isabloi  29535  smcnlem  29681  cncph  29803  hvsubf  29999  hhip  30161  hhph  30162  helch  30227  hsn0elch  30232  hhssabloilem  30245  hhshsslem2  30252  shscli  30301  shintcli  30313  pjmf1  30700  idunop  30962  0cnop  30963  0cnfn  30964  idcnop  30965  idhmop  30966  0hmop  30967  adj0  30978  lnophsi  30985  lnopunii  30996  lnophmi  31002  nlelshi  31044  riesz4i  31047  cnlnadjlem6  31056  cnlnadjlem9  31059  adjcoi  31084  bra11  31092  pjhmopi  31130  iundisj2f  31550  iundisj2fi  31742  xrstos  31912  xrge0omnd  31961  reofld  32176  xrge0slmod  32180  iistmd  32523  cnre2csqima  32532  mndpluscn  32547  raddcn  32550  xrge0iifiso  32556  xrge0iifmhm  32560  xrge0pluscn  32561  cnzh  32591  rezh  32592  br2base  32909  sxbrsiga  32930  signswmnd  33209  cardpred  33734  nummin  33735  indispconn  33868  cnllysconn  33879  ioosconn  33881  rellysconn  33885  fmlaomn0  34024  gonan0  34026  goaln0  34027  fneref  34851  dnicn  34984  f1omptsnlem  35836  isbasisrelowl  35858  poimirlem27  36134  mblfinlem1  36144  mblfinlem2  36145  exidu1  36344  rngoideu  36391  isomliN  37730  idlaut  38588  resubf  40879  sn-subf  40926  mzpclall  41079  frmx  41266  frmy  41267  kelac2lem  41420  onsucf1o  41636  ontric3g  41868  clsk1indlem3  42389  icof  43514  natglobalincr  45190  sprsymrelf1  45762  fmtnof1  45801  prmdvdsfmtnof1  45853  uspgrsprf1  46123  plusfreseq  46140  nnsgrpmgm  46184  nnsgrp  46185  nn0mnd  46187  2zrngamgm  46311  2zrngmmgm  46318  2zrngnmrid  46322  ldepslinc  46664  rrx2xpref1o  46878  rrx2plordisom  46883
  Copyright terms: Public domain W3C validator