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

Theorem 2ralbidva 2983
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 679 . . 3 (((𝜑𝑥𝐴) ∧ 𝑦𝐵) → (𝜓𝜒))
32ralbidva 2980 . 2 ((𝜑𝑥𝐴) → (∀𝑦𝐵 𝜓 ↔ ∀𝑦𝐵 𝜒))
43ralbidva 2980 1 (𝜑 → (∀𝑥𝐴𝑦𝐵 𝜓 ↔ ∀𝑥𝐴𝑦𝐵 𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 384  wcel 1987  wral 2907
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836
This theorem depends on definitions:  df-bi 197  df-an 386  df-ral 2912
This theorem is referenced by:  disjxun  4616  isocnv3  6542  isotr  6546  f1oweALT  7104  fnmpt2ovd  7204  tosso  16964  pospropd  17062  isipodrs  17089  mndpropd  17244  mhmpropd  17269  efgred  18089  cmnpropd  18130  ringpropd  18510  lmodprop2d  18853  lsspropd  18945  islmhm2  18966  lmhmpropd  19001  assapropd  19255  islindf4  20105  scmatmats  20245  cpmatel2  20446  1elcpmat  20448  m2cpminvid2  20488  decpmataa0  20501  pmatcollpw2lem  20510  connsub  21143  hausdiag  21367  ist0-4  21451  ismet2  22057  txmetcnp  22271  txmetcn  22272  metuel2  22289  metucn  22295  isngp3  22321  nlmvscn  22410  isclmp  22816  isncvsngp  22868  ipcn  22964  iscfil2  22983  caucfil  23000  cfilresi  23012  ulmdvlem3  24073  cxpcn3  24402  tgcgr4  25339  perpcom  25521  brbtwn2  25698  colinearalglem2  25700  eengtrkg  25778  isarchi2  29542  elmrsubrn  31152  isbnd3b  33243  iscvlat2N  34118  ishlat3N  34148  gicabl  37176  isdomn3  37290  mgmpropd  41084  mgmhmpropd  41094  lidlmmgm  41234  lindslinindsimp2  41561
  Copyright terms: Public domain W3C validator