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

Theorem 2ralbidva 2971
 Description: Formula-building rule for restricted universal quantifiers (deduction rule). (Contributed by NM, 4-Mar-1997.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 9-Dec-2019.)
Hypothesis
Ref Expression
2ralbidva.1 ((𝜑 ∧ (𝑥𝐴𝑦𝐵)) → (𝜓𝜒))
Assertion
Ref Expression
2ralbidva (𝜑 → (∀𝑥𝐴𝑦𝐵 𝜓 ↔ ∀𝑥𝐴𝑦𝐵 𝜒))
Distinct variable groups:   𝑥,𝑦,𝜑   𝑦,𝐴
Allowed substitution hints:   𝜓(𝑥,𝑦)   𝜒(𝑥,𝑦)   𝐴(𝑥)   𝐵(𝑥,𝑦)

Proof of Theorem 2ralbidva
StepHypRef Expression
1 2ralbidva.1 . . . 4 ((𝜑 ∧ (𝑥𝐴𝑦𝐵)) → (𝜓𝜒))
21anassrs 678 . . 3 (((𝜑𝑥𝐴) ∧ 𝑦𝐵) → (𝜓𝜒))
32ralbidva 2968 . 2 ((𝜑𝑥𝐴) → (∀𝑦𝐵 𝜓 ↔ ∀𝑦𝐵 𝜒))
43ralbidva 2968 1 (𝜑 → (∀𝑥𝐴𝑦𝐵 𝜓 ↔ ∀𝑥𝐴𝑦𝐵 𝜒))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 195   ∧ wa 383   ∈ 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 This theorem depends on definitions:  df-bi 196  df-an 385  df-ral 2901 This theorem is referenced by:  disjxun  4581  isocnv3  6482  isotr  6486  f1oweALT  7043  fnmpt2ovd  7139  tosso  16859  pospropd  16957  isipodrs  16984  mndpropd  17139  mhmpropd  17164  efgred  17984  cmnpropd  18025  ringpropd  18405  lmodprop2d  18748  lsspropd  18838  islmhm2  18859  lmhmpropd  18894  assapropd  19148  islindf4  19996  scmatmats  20136  cpmatel2  20337  1elcpmat  20339  m2cpminvid2  20379  decpmataa0  20392  pmatcollpw2lem  20401  connsub  21034  hausdiag  21258  ist0-4  21342  ismet2  21948  txmetcnp  22162  txmetcn  22163  metuel2  22180  metucn  22186  isngp3  22212  nlmvscn  22301  isclmp  22705  isncvsngp  22757  ipcn  22853  iscfil2  22872  caucfil  22889  cfilresi  22901  ulmdvlem3  23960  cxpcn3  24289  tgcgr4  25226  perpcom  25408  brbtwn2  25585  colinearalglem2  25587  eengtrkg  25665  isarchi2  29070  elmrsubrn  30671  isbnd3b  32754  iscvlat2N  33629  ishlat3N  33659  gicabl  36687  isdomn3  36801  mgmpropd  41565  mgmhmpropd  41575  lidlmmgm  41715  lindslinindsimp2  42046
 Copyright terms: Public domain W3C validator