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

Theorem ralbii2 2961
 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 1737 . 2 (∀𝑥(𝑥𝐴𝜑) ↔ ∀𝑥(𝑥𝐵𝜓))
3 df-ral 2901 . 2 (∀𝑥𝐴 𝜑 ↔ ∀𝑥(𝑥𝐴𝜑))
4 df-ral 2901 . 2 (∀𝑥𝐵 𝜓 ↔ ∀𝑥(𝑥𝐵𝜓))
52, 3, 43bitr4i 291 1 (∀𝑥𝐴 𝜑 ↔ ∀𝑥𝐵 𝜓)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 195  ∀wal 1473   ∈ wcel 1977  ∀wral 2896 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728 This theorem depends on definitions:  df-bi 196  df-ral 2901 This theorem is referenced by:  ralbiia  2962  ralbii  2963  raleqbii  2973  ralrab  3335  raldifb  3712  raldifsni  4265  reusv2  4800  dfsup2  8233  iscard2  8685  acnnum  8758  dfac9  8841  dfacacn  8846  raluz2  11613  ralrp  11728  isprm4  15235  isdomn2  19120  isnrm2  20972  ismbl  23101  ellimc3  23449  dchrelbas2  24762  h1dei  27793  fnwe2lem2  36639  sdrgacs  36790
 Copyright terms: Public domain W3C validator