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

Theorem ralbidv2 2733
 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:   ,
Allowed substitution hints:   ()   ()   ()   ()

Proof of Theorem ralbidv2
StepHypRef Expression
1 ralbidv2.1 . . 3
21albidv 1636 . 2
3 df-ral 2716 . 2
4 df-ral 2716 . 2
52, 3, 43bitr4g 281 1
 Colors of variables: wff set class Syntax hints:   wi 4   wb 178  wal 1550   wcel 1727  wral 2711 This theorem is referenced by:  ralss  3395  oneqmini  4661  ordunisuc2  4853  dfsmo2  6638  wemapso2lem  7548  zorn2lem1  8407  raluz  10556  limsupgle  12302  ello12  12341  elo12  12352  lo1resb  12389  rlimresb  12390  o1resb  12391  isprm3  13119  ist1  17416  ist1-2  17442  hausdiag  17708  xkopt  17718  cnflf  18065  cnfcf  18105  metcnp  18602  caucfil  19267  mdegleb  20018  filnetlem4  26448 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627 This theorem depends on definitions:  df-bi 179  df-ral 2716
 Copyright terms: Public domain W3C validator