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

Theorem ralbii2 3160
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 1811 . 2 (∀𝑥(𝑥𝐴𝜑) ↔ ∀𝑥(𝑥𝐵𝜓))
3 df-ral 3140 . 2 (∀𝑥𝐴 𝜑 ↔ ∀𝑥(𝑥𝐴𝜑))
4 df-ral 3140 . 2 (∀𝑥𝐵 𝜓 ↔ ∀𝑥(𝑥𝐵𝜓))
52, 3, 43bitr4i 304 1 (∀𝑥𝐴 𝜑 ↔ ∀𝑥𝐵 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207  wal 1526  wcel 2105  wral 3135
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801
This theorem depends on definitions:  df-bi 208  df-ral 3140
This theorem is referenced by:  ralbiia  3161  ralbii  3162  raleqbii  3231  ralrab  3682  raldifb  4118  raldifsni  4720  reusv2  5294  dfsup2  8896  iscard2  9393  acnnum  9466  dfac9  9550  dfacacn  9555  raluz2  12285  ralrp  12397  isprm4  16016  sdrgacs  19509  isdomn2  20000  isnrm2  21894  ismbl  24054  ellimc3  24404  dchrelbas2  25740  h1dei  29254  fnwe2lem2  39529
  Copyright terms: Public domain W3C validator