ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  rgen2 GIF version

Theorem rgen2 2563
Description: Generalization rule for restricted quantification. (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 2550 . 2 (𝑥𝐴 → ∀𝑦𝐵 𝜑)
32rgen 2530 1 𝑥𝐴𝑦𝐵 𝜑
Colors of variables: wff set class
Syntax hints:  wi 4  wa 104  wcel 2148  wral 2455
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1447  ax-gen 1449  ax-4 1510  ax-17 1526
This theorem depends on definitions:  df-bi 117  df-nf 1461  df-ral 2460
This theorem is referenced by:  rgen3  2564  f1stres  6154  f2ndres  6155  exmidonfinlem  7186  netap  7243  2onetap  7244  2omotaplemap  7246  divfnzn  9607  1arith  12345  mgmidmo  12680  isabli  12927  txuni2  13416  divcnap  13715  abscncf  13732  recncf  13733  imcncf  13734  cjcncf  13735  reefiso  13858  ioocosf1o  13935
  Copyright terms: Public domain W3C validator