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

Theorem 2ralbidva 3207
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 469 . . 3 (((𝜑𝑥𝐴) ∧ 𝑦𝐵) → (𝜓𝜒))
32ralbidva 3169 . 2 ((𝜑𝑥𝐴) → (∀𝑦𝐵 𝜓 ↔ ∀𝑦𝐵 𝜒))
43ralbidva 3169 1 (𝜑 → (∀𝑥𝐴𝑦𝐵 𝜓 ↔ ∀𝑥𝐴𝑦𝐵 𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 397  wcel 2107  wral 3061
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914
This theorem depends on definitions:  df-bi 206  df-an 398  df-ral 3062
This theorem is referenced by:  disjxun  5104  reu3op  6245  opreu2reurex  6247  isocnv3  7278  isotr  7282  f1oweALT  7906  fnmpoovd  8020  pospropd  18221  tosso  18313  isipodrs  18431  mndpropd  18586  mhmpropd  18613  efgred  19535  cmnpropd  19578  ringpropd  20011  lmodprop2d  20399  lsspropd  20493  islmhm2  20514  lmhmpropd  20549  islindf4  21260  assapropd  21291  scmatmats  21876  cpmatel2  22078  1elcpmat  22080  m2cpminvid2  22120  decpmataa0  22133  pmatcollpw2lem  22142  connsub  22788  hausdiag  23012  ist0-4  23096  ismet2  23702  txmetcnp  23919  txmetcn  23920  metuel2  23937  metucn  23943  isngp3  23970  nlmvscn  24067  isclmp  24476  isncvsngp  24529  ipcn  24626  iscfil2  24646  caucfil  24663  cfilresi  24675  ulmdvlem3  25777  cxpcn3  26117  tgjustf  27457  tgjustr  27458  tgcgr4  27515  perpcom  27697  brbtwn2  27896  colinearalglem2  27898  eengtrkg  27977  isarchi2  32070  elmrsubrn  34171  isbnd3b  36290  iscvlat2N  37832  ishlat3N  37862  gicabl  41469  isdomn3  41574  mgmpropd  46155  mgmhmpropd  46165  lidlmmgm  46309  lindslinindsimp2  46630  joindm3  47088  meetdm3  47090  functhinclem1  47147  postc  47188
  Copyright terms: Public domain W3C validator