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

Theorem ralbidv2 2892
Description: Formula-building rule for restricted universal quantifier (deduction rule). (Contributed by NM, 6-Apr-1997.)
Hypothesis
Ref Expression
ralbidv2.1
Assertion
Ref Expression
ralbidv2
Distinct variable group:   ,

Proof of Theorem ralbidv2
StepHypRef Expression
1 ralbidv2.1 . . 3
21albidv 1713 . 2
3 df-ral 2812 . 2
4 df-ral 2812 . 2
52, 3, 43bitr4g 288 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184  A.wal 1393  e.wcel 1818  A.wral 2807
This theorem is referenced by:  ralbidva  2893  ralss  3565  oneqmini  4934  ordunisuc2  6679  dfsmo2  7037  wemapsolem  7996  zorn2lem1  8897  raluz  11158  limsupgle  13300  ello12  13339  elo12  13350  lo1resb  13387  rlimresb  13388  o1resb  13389  isprm3  14226  ist1  19822  ist1-2  19848  hausdiag  20146  xkopt  20156  cnflf  20503  cnfcf  20543  metcnp  21044  caucfil  21722  mdegleb  22464  eulerpartlemgvv  28315  filnetlem4  30199  isprm7  31192
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704
This theorem depends on definitions:  df-bi 185  df-ral 2812
  Copyright terms: Public domain W3C validator