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

Theorem raleqbidva 3326
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 3174 . 2 (𝜑 → (∀𝑥𝐴 𝜓 ↔ ∀𝑥𝐴 𝜒))
3 raleqbidva.1 . . 3 (𝜑𝐴 = 𝐵)
43raleqdv 3324 . 2 (𝜑 → (∀𝑥𝐴 𝜒 ↔ ∀𝑥𝐵 𝜒))
52, 4bitrd 279 1 (𝜑 → (∀𝑥𝐴 𝜓 ↔ ∀𝑥𝐵 𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 395   = wceq 1540  wcel 2105  wral 3060
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-9 2115  ax-ext 2702
This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1781  df-cleq 2723  df-ral 3061  df-rex 3070
This theorem is referenced by:  raleqbidvv  3328  catpropd  17658  cidpropd  17659  funcpropd  17856  fullpropd  17876  natpropd  17934  gsumpropd2lem  18605  ringurd  20080  istrkgcb  27975  iscgrg  28031  isperp  28231  clwlkclwwlk  29523  urpropd  32649  lindfpropd  32773  opprqus0g  32879  opprqusdrng  32882  ist0cld  33112  matunitlindflem1  36788  sticksstones3  41271  sticksstones11  41279
  Copyright terms: Public domain W3C validator