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

Theorem ralbii2 3130
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 1801 . 2 (∀𝑥(𝑥𝐴𝜑) ↔ ∀𝑥(𝑥𝐵𝜓))
3 df-ral 3110 . 2 (∀𝑥𝐴 𝜑 ↔ ∀𝑥(𝑥𝐴𝜑))
4 df-ral 3110 . 2 (∀𝑥𝐵 𝜓 ↔ ∀𝑥(𝑥𝐵𝜓))
52, 3, 43bitr4i 304 1 (∀𝑥𝐴 𝜑 ↔ ∀𝑥𝐵 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207  wal 1520  wcel 2081  wral 3105
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791
This theorem depends on definitions:  df-bi 208  df-ral 3110
This theorem is referenced by:  ralbiia  3131  ralbii  3132  raleqbii  3198  ralrab  3623  raldifb  4042  raldifsni  4635  reusv2  5195  dfsup2  8754  iscard2  9251  acnnum  9324  dfac9  9408  dfacacn  9413  raluz2  12146  ralrp  12259  isprm4  15857  sdrgacs  19270  isdomn2  19761  isnrm2  21650  ismbl  23810  ellimc3  24160  dchrelbas2  25495  h1dei  29018  fnwe2lem2  39136
  Copyright terms: Public domain W3C validator