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

Theorem 2ralbidva 3126
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 683 . . 3 (((𝜑𝑥𝐴) ∧ 𝑦𝐵) → (𝜓𝜒))
32ralbidva 3123 . 2 ((𝜑𝑥𝐴) → (∀𝑦𝐵 𝜓 ↔ ∀𝑦𝐵 𝜒))
43ralbidva 3123 1 (𝜑 → (∀𝑥𝐴𝑦𝐵 𝜓 ↔ ∀𝑥𝐴𝑦𝐵 𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 383  wcel 2139  wral 3050
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988
This theorem depends on definitions:  df-bi 197  df-an 385  df-ral 3055
This theorem is referenced by:  disjxun  4802  isocnv3  6745  isotr  6749  f1oweALT  7317  fnmpt2ovd  7420  tosso  17237  pospropd  17335  isipodrs  17362  mndpropd  17517  mhmpropd  17542  efgred  18361  cmnpropd  18402  ringpropd  18782  lmodprop2d  19127  lsspropd  19219  islmhm2  19240  lmhmpropd  19275  assapropd  19529  islindf4  20379  scmatmats  20519  cpmatel2  20720  1elcpmat  20722  m2cpminvid2  20762  decpmataa0  20775  pmatcollpw2lem  20784  connsub  21426  hausdiag  21650  ist0-4  21734  ismet2  22339  txmetcnp  22553  txmetcn  22554  metuel2  22571  metucn  22577  isngp3  22603  nlmvscn  22692  isclmp  23097  isncvsngp  23149  ipcn  23245  iscfil2  23264  caucfil  23281  cfilresi  23293  ulmdvlem3  24355  cxpcn3  24688  tgcgr4  25625  perpcom  25807  brbtwn2  25984  colinearalglem2  25986  eengtrkg  26064  isarchi2  30048  elmrsubrn  31724  isbnd3b  33897  iscvlat2N  35114  ishlat3N  35144  gicabl  38171  isdomn3  38284  mgmpropd  42285  mgmhmpropd  42295  lidlmmgm  42435  lindslinindsimp2  42762
  Copyright terms: Public domain W3C validator