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

Theorem ralbii2 3089
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 1819 . 2 (∀𝑥(𝑥𝐴𝜑) ↔ ∀𝑥(𝑥𝐵𝜓))
3 df-ral 3062 . 2 (∀𝑥𝐴 𝜑 ↔ ∀𝑥(𝑥𝐴𝜑))
4 df-ral 3062 . 2 (∀𝑥𝐵 𝜓 ↔ ∀𝑥(𝑥𝐵𝜓))
52, 3, 43bitr4i 303 1 (∀𝑥𝐴 𝜑 ↔ ∀𝑥𝐵 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wal 1538  wcel 2108  wral 3061
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809
This theorem depends on definitions:  df-bi 207  df-ral 3062
This theorem is referenced by:  ralbiia  3091  ralcom3  3097  raleqbii  3344  ralrab  3699  raldifb  4149  ralin  4249  raldifsni  4795  reusv2  5403  dfsup2  9484  iscard2  10016  acnnum  10092  dfac9  10177  dfacacn  10182  raluz2  12939  ralrp  13055  isprm4  16721  isdomn2OLD  20712  sdrgacs  20802  isnrm2  23366  ismbl  25561  ellimc3  25914  dchrelbas2  27281  h1dei  31569  iineq1i  36197  ixpeq1i  36201  fnwe2lem2  43063
  Copyright terms: Public domain W3C validator