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

Theorem raleqbidva 3131
 Description: Equality deduction for restricted universal quantifier. (Contributed by Mario Carneiro, 5-Jan-2017.)
Hypotheses
Ref Expression
raleqbidva.1 (𝜑𝐴 = 𝐵)
raleqbidva.2 ((𝜑𝑥𝐴) → (𝜓𝜒))
Assertion
Ref Expression
raleqbidva (𝜑 → (∀𝑥𝐴 𝜓 ↔ ∀𝑥𝐵 𝜒))
Distinct variable groups:   𝑥,𝐴   𝑥,𝐵   𝜑,𝑥
Allowed substitution hints:   𝜓(𝑥)   𝜒(𝑥)

Proof of Theorem raleqbidva
StepHypRef Expression
1 raleqbidva.2 . . 3 ((𝜑𝑥𝐴) → (𝜓𝜒))
21ralbidva 2968 . 2 (𝜑 → (∀𝑥𝐴 𝜓 ↔ ∀𝑥𝐴 𝜒))
3 raleqbidva.1 . . 3 (𝜑𝐴 = 𝐵)
43raleqdv 3121 . 2 (𝜑 → (∀𝑥𝐴 𝜒 ↔ ∀𝑥𝐵 𝜒))
52, 4bitrd 267 1 (𝜑 → (∀𝑥𝐴 𝜓 ↔ ∀𝑥𝐵 𝜒))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 195   ∧ wa 383   = wceq 1475   ∈ 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  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-ext 2590 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ral 2901 This theorem is referenced by:  catpropd  16192  cidpropd  16193  funcpropd  16383  fullpropd  16403  natpropd  16459  gsumpropd2lem  17096  istrkgc  25153  istrkgb  25154  istrkgcb  25155  istrkge  25156  iscgrg  25207  isperp  25407  clwlkisclwwlk  26317  rngurd  29119  matunitlindflem1  32575  clwlkclwwlk  41211
 Copyright terms: Public domain W3C validator