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

Theorem ralbii2 3131
 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 1821 . 2 (∀𝑥(𝑥𝐴𝜑) ↔ ∀𝑥(𝑥𝐵𝜓))
3 df-ral 3111 . 2 (∀𝑥𝐴 𝜑 ↔ ∀𝑥(𝑥𝐴𝜑))
4 df-ral 3111 . 2 (∀𝑥𝐵 𝜓 ↔ ∀𝑥(𝑥𝐵𝜓))
52, 3, 43bitr4i 306 1 (∀𝑥𝐴 𝜑 ↔ ∀𝑥𝐵 𝜓)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209  ∀wal 1536   ∈ wcel 2111  ∀wral 3106 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811 This theorem depends on definitions:  df-bi 210  df-ral 3111 This theorem is referenced by:  ralbiia  3132  ralbii  3133  raleqbii  3197  ralrab  3633  raldifb  4072  raldifsni  4688  reusv2  5269  dfsup2  8894  iscard2  9391  acnnum  9465  dfac9  9549  dfacacn  9554  raluz2  12287  ralrp  12399  isprm4  16020  sdrgacs  19576  isdomn2  20068  isnrm2  21970  ismbl  24137  ellimc3  24489  dchrelbas2  25828  h1dei  29340  fnwe2lem2  40010
 Copyright terms: Public domain W3C validator