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

Theorem raleqbidva 3301
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 3131 . 2 (𝜑 → (∀𝑥𝐴 𝜓 ↔ ∀𝑥𝐴 𝜒))
3 raleqbidva.1 . . 3 (𝜑𝐴 = 𝐵)
43raleqdv 3291 . 2 (𝜑 → (∀𝑥𝐴 𝜒 ↔ ∀𝑥𝐵 𝜒))
52, 4bitrd 270 1 (𝜑 → (∀𝑥𝐴 𝜓 ↔ ∀𝑥𝐵 𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197  wa 384   = wceq 1652  wcel 2155  wral 3054
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2069  ax-7 2105  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-ext 2742
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-tru 1656  df-ex 1875  df-nf 1879  df-cleq 2757  df-clel 2760  df-nfc 2895  df-ral 3059
This theorem is referenced by:  catpropd  16635  cidpropd  16636  funcpropd  16826  fullpropd  16846  natpropd  16902  gsumpropd2lem  17540  istrkgc  25643  istrkgb  25644  istrkgcb  25645  istrkge  25646  iscgrg  25697  isperp  25897  clwlkclwwlk  27207  rngurd  30169  matunitlindflem1  33761
  Copyright terms: Public domain W3C validator