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

Theorem rgen2 3190
 Description: Generalization rule for restricted quantification, with two quantifiers. This theorem should be used in place of rgen2a 3216 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 3169 . 2 (𝑥𝐴 → ∀𝑦𝐵 𝜑)
32rgen 3135 1 𝑥𝐴𝑦𝐵 𝜑
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 398   ∈ wcel 2114  ∀wral 3125 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911 This theorem depends on definitions:  df-bi 209  df-an 399  df-ral 3130 This theorem is referenced by:  rgen3  3191  invdisjrabw  5027  invdisjrab  5028  sosn  5614  isoid  7059  f1owe  7083  epweon  7475  f1stres  7691  f2ndres  7692  fnwelem  7803  issmo  7963  oawordeulem  8158  ecopover  8379  unfilem2  8761  dffi2  8865  inficl  8867  fipwuni  8868  fisn  8869  dffi3  8873  cantnfvalf  9106  r111  9182  alephf1  9489  alephiso  9502  dfac5lem4  9530  kmlem9  9562  ackbij1lem17  9636  fin1a2lem2  9801  fin1a2lem4  9803  axcc2lem  9836  smobeth  9986  nqereu  10329  addpqf  10344  mulpqf  10346  genpdm  10402  axaddf  10545  axmulf  10546  subf  10866  mulnzcnopr  11264  negiso  11599  cnref1o  12363  xaddf  12596  xmulf  12644  ioof  12816  om2uzf1oi  13305  om2uzisoi  13306  wrd2ind  14065  wwlktovf1  14301  reeff1  15453  divalglem9  15730  bitsf1  15773  smupf  15805  gcdf  15839  eucalgf  15905  qredeu  15980  1arith  16241  vdwapf  16286  xpsff1o  16819  catideu  16925  sscres  17072  fpwipodrs  17753  letsr  17816  mgmidmo  17849  frmdplusg  17998  efmndmgm  18029  smndex1mgm  18051  pwmnd  18081  mulgfval  18205  nmznsg  18299  efgmf  18818  efglem  18821  efgred  18853  isabli  18900  brric  19475  xrsmgm  20556  xrs1cmn  20561  xrge0subm  20562  xrsds  20564  cnsubmlem  20569  cnsubrglem  20571  nn0srg  20591  rge0srg  20592  rzgrp  20743  fibas  21561  fctop  21588  cctop  21590  iccordt  21798  txuni2  22149  fsubbas  22451  zfbas  22480  ismeti  22911  dscmet  23158  qtopbaslem  23343  tgqioo  23384  xrsxmet  23393  xrsdsre  23394  retopconn  23413  iccconn  23414  divcn  23452  abscncf  23485  recncf  23486  imcncf  23487  cjcncf  23488  iimulcn  23522  icopnfhmeo  23527  iccpnfhmeo  23529  xrhmeo  23530  cnllycmp  23540  bndth  23542  iundisj2  24132  dyadf  24174  reefiso  25022  recosf1o  25106  cxpcn3  25316  sgmf  25709  2lgslem1b  25955  tgjustf  26246  ercgrg  26290  2wspmdisj  28101  isabloi  28313  smcnlem  28459  cncph  28581  hvsubf  28777  hhip  28939  hhph  28940  helch  29005  hsn0elch  29010  hhssabloilem  29023  hhshsslem2  29030  shscli  29079  shintcli  29091  pjmf1  29478  idunop  29740  0cnop  29741  0cnfn  29742  idcnop  29743  idhmop  29744  0hmop  29745  adj0  29756  lnophsi  29763  lnopunii  29774  lnophmi  29780  nlelshi  29822  riesz4i  29825  cnlnadjlem6  29834  cnlnadjlem9  29837  adjcoi  29862  bra11  29870  pjhmopi  29908  iundisj2f  30327  iundisj2fi  30507  xrstos  30674  xrge0omnd  30720  reofld  30921  xrge0slmod  30925  iistmd  31153  cnre2csqima  31162  mndpluscn  31177  raddcn  31180  xrge0iifiso  31186  xrge0iifmhm  31190  xrge0pluscn  31191  cnzh  31219  rezh  31220  br2base  31535  sxbrsiga  31556  signswmnd  31835  indispconn  32489  cnllysconn  32500  ioosconn  32502  rellysconn  32506  fmlaomn0  32645  gonan0  32647  goaln0  32648  soseq  33104  fneref  33706  dnicn  33839  f1omptsnlem  34634  isbasisrelowl  34656  poimirlem27  34960  mblfinlem1  34970  mblfinlem2  34971  exidu1  35170  rngoideu  35217  isomliN  36411  idlaut  37268  resubf  39331  sn-subf  39376  mzpclall  39461  frmx  39647  frmy  39648  kelac2lem  39801  ontric3g  40023  clsk1indlem3  40528  icof  41636  sprsymrelf1  43804  fmtnof1  43843  prmdvdsfmtnof1  43895  uspgrsprf1  44167  plusfreseq  44184  nnsgrpmgm  44228  nnsgrp  44229  nn0mnd  44231  2zrngamgm  44355  2zrngmmgm  44362  2zrngnmrid  44366  ldepslinc  44709  rrx2xpref1o  44892  rrx2plordisom  44897
 Copyright terms: Public domain W3C validator