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

Theorem ralbii2 3007
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 1787 . 2 (∀𝑥(𝑥𝐴𝜑) ↔ ∀𝑥(𝑥𝐵𝜓))
3 df-ral 2946 . 2 (∀𝑥𝐴 𝜑 ↔ ∀𝑥(𝑥𝐴𝜑))
4 df-ral 2946 . 2 (∀𝑥𝐵 𝜓 ↔ ∀𝑥(𝑥𝐵𝜓))
52, 3, 43bitr4i 292 1 (∀𝑥𝐴 𝜑 ↔ ∀𝑥𝐵 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wal 1521  wcel 2030  wral 2941
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777
This theorem depends on definitions:  df-bi 197  df-ral 2946
This theorem is referenced by:  ralbiia  3008  ralbii  3009  raleqbii  3019  ralrab  3401  raldifb  3783  raldifsni  4357  reusv2  4904  dfsup2  8391  iscard2  8840  acnnum  8913  dfac9  8996  dfacacn  9001  raluz2  11775  ralrp  11890  isprm4  15444  isdomn2  19347  isnrm2  21210  ismbl  23340  ellimc3  23688  dchrelbas2  25007  h1dei  28537  fnwe2lem2  37938  sdrgacs  38088
  Copyright terms: Public domain W3C validator