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

Theorem 2ralbidva 3206
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 466 . . 3 (((𝜑𝑥𝐴) ∧ 𝑦𝐵) → (𝜓𝜒))
32ralbidva 3165 . 2 ((𝜑𝑥𝐴) → (∀𝑦𝐵 𝜓 ↔ ∀𝑦𝐵 𝜒))
43ralbidva 3165 1 (𝜑 → (∀𝑥𝐴𝑦𝐵 𝜓 ↔ ∀𝑥𝐴𝑦𝐵 𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 394  wcel 2098  wral 3050
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905
This theorem depends on definitions:  df-bi 206  df-an 395  df-ral 3051
This theorem is referenced by:  disjxun  5147  reu3op  6298  opreu2reurex  6300  isocnv3  7339  isotr  7343  f1oweALT  7977  fnmpoovd  8092  pospropd  18322  tosso  18414  isipodrs  18532  mgmpropd  18614  mgmhmpropd  18661  sgrppropd  18694  mndpropd  18722  mhmpropd  18752  efgred  19715  cmnpropd  19758  rngpropd  20126  ringpropd  20236  lmodprop2d  20819  lsspropd  20914  islmhm2  20935  lmhmpropd  20970  isdomn3  21265  islindf4  21789  assapropd  21822  scmatmats  22457  cpmatel2  22659  1elcpmat  22661  m2cpminvid2  22701  decpmataa0  22714  pmatcollpw2lem  22723  connsub  23369  hausdiag  23593  ist0-4  23677  ismet2  24283  txmetcnp  24500  txmetcn  24501  metuel2  24518  metucn  24524  isngp3  24551  nlmvscn  24648  isclmp  25068  isncvsngp  25121  ipcn  25218  iscfil2  25238  caucfil  25255  cfilresi  25267  ulmdvlem3  26383  cxpcn3  26728  tgjustf  28349  tgjustr  28350  tgcgr4  28407  perpcom  28589  brbtwn2  28788  colinearalglem2  28790  eengtrkg  28869  isarchi2  32985  opprlidlabs  33297  elmrsubrn  35261  isbnd3b  37389  iscvlat2N  38926  ishlat3N  38956  gicabl  42665  lindslinindsimp2  47717  joindm3  48174  meetdm3  48176  functhinclem1  48233  postc  48274
  Copyright terms: Public domain W3C validator