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

Theorem 2ralbidva 3148
Description: Formula-building rule for restricted universal quantifiers (deduction form). (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 460 . . 3 (((𝜑𝑥𝐴) ∧ 𝑦𝐵) → (𝜓𝜒))
32ralbidva 3146 . 2 ((𝜑𝑥𝐴) → (∀𝑦𝐵 𝜓 ↔ ∀𝑦𝐵 𝜒))
43ralbidva 3146 1 (𝜑 → (∀𝑥𝐴𝑦𝐵 𝜓 ↔ ∀𝑥𝐴𝑦𝐵 𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 198  wa 387  wcel 2050  wral 3088
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869
This theorem depends on definitions:  df-bi 199  df-an 388  df-ral 3093
This theorem is referenced by:  disjxun  4927  reu3op  5981  opreu2reurex  5983  isocnv3  6908  isotr  6912  f1oweALT  7485  fnmpoovd  7590  tosso  17504  pospropd  17602  isipodrs  17629  mndpropd  17784  mhmpropd  17809  efgred  18634  cmnpropd  18675  ringpropd  19055  lmodprop2d  19418  lsspropd  19511  islmhm2  19532  lmhmpropd  19567  assapropd  19821  islindf4  20684  scmatmats  20824  cpmatel2  21025  1elcpmat  21027  m2cpminvid2  21067  decpmataa0  21080  pmatcollpw2lem  21089  connsub  21733  hausdiag  21957  ist0-4  22041  ismet2  22646  txmetcnp  22860  txmetcn  22861  metuel2  22878  metucn  22884  isngp3  22910  nlmvscn  22999  isclmp  23404  isncvsngp  23456  ipcn  23552  iscfil2  23572  caucfil  23589  cfilresi  23601  ulmdvlem3  24693  cxpcn3  25030  tgjustf  25961  tgjustr  25962  tgcgr4  26019  perpcom  26201  brbtwn2  26394  colinearalglem2  26396  eengtrkg  26475  isarchi2  30486  elmrsubrn  32293  isbnd3b  34511  iscvlat2N  35911  ishlat3N  35941  gicabl  39101  isdomn3  39206  mgmpropd  43416  mgmhmpropd  43426  lidlmmgm  43566  lindslinindsimp2  43891
  Copyright terms: Public domain W3C validator