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

Theorem ralbii2 2886
Description: Inference adding different restricted universal quantifiers to each side of an equivalence. (Contributed by NM, 15-Aug-2005.)
Hypothesis
Ref Expression
ralbii2.1
Assertion
Ref Expression
ralbii2

Proof of Theorem ralbii2
StepHypRef Expression
1 ralbii2.1 . . 3
21albii 1640 . 2
3 df-ral 2812 . 2
4 df-ral 2812 . 2
52, 3, 43bitr4i 277 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:  ralbiia  2887  ralbii  2888  raleqbii  2902  ralrab  3261  raldifb  3643  raldifsni  4160  reusv2  4658  dfsup2  7922  iscard2  8378  acnnum  8454  dfac9  8537  dfacacn  8542  raluz2  11159  ralrp  11267  isprm4  14227  isdomn2  17948  isnrm2  19859  ismbl  21937  ellimc3  22283  dchrelbas2  23512  h1dei  26468  fnwe2lem2  30997  sdrgacs  31150
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631
This theorem depends on definitions:  df-bi 185  df-ral 2812
  Copyright terms: Public domain W3C validator