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

Theorem 2ralbidva 3219
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 467 . . 3 (((𝜑𝑥𝐴) ∧ 𝑦𝐵) → (𝜓𝜒))
32ralbidva 3176 . 2 ((𝜑𝑥𝐴) → (∀𝑦𝐵 𝜓 ↔ ∀𝑦𝐵 𝜒))
43ralbidva 3176 1 (𝜑 → (∀𝑥𝐴𝑦𝐵 𝜓 ↔ ∀𝑥𝐴𝑦𝐵 𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395  wcel 2108  wral 3061
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910
This theorem depends on definitions:  df-bi 207  df-an 396  df-ral 3062
This theorem is referenced by:  disjxun  5141  reu3op  6312  opreu2reurex  6314  isocnv3  7352  isotr  7356  f1oweALT  7997  fnmpoovd  8112  pospropd  18372  tosso  18464  isipodrs  18582  mgmpropd  18664  mgmhmpropd  18711  sgrppropd  18744  mndpropd  18772  mhmpropd  18805  efgred  19766  cmnpropd  19809  rngpropd  20171  ringpropd  20285  isdomn3  20715  lmodprop2d  20922  lsspropd  21016  islmhm2  21037  lmhmpropd  21072  islindf4  21858  assapropd  21892  scmatmats  22517  cpmatel2  22719  1elcpmat  22721  m2cpminvid2  22761  decpmataa0  22774  pmatcollpw2lem  22783  connsub  23429  hausdiag  23653  ist0-4  23737  ismet2  24343  txmetcnp  24560  txmetcn  24561  metuel2  24578  metucn  24584  isngp3  24611  nlmvscn  24708  isclmp  25130  isncvsngp  25183  ipcn  25280  iscfil2  25300  caucfil  25317  cfilresi  25329  ulmdvlem3  26445  cxpcn3  26791  tgjustf  28481  tgjustr  28482  tgcgr4  28539  perpcom  28721  brbtwn2  28920  colinearalglem2  28922  eengtrkg  29001  isarchi2  33192  opprlidlabs  33513  elmrsubrn  35525  isbnd3b  37792  iscvlat2N  39325  ishlat3N  39355  gicabl  43111  lindslinindsimp2  48380  joindm3  48866  meetdm3  48868  fucofulem2  49006  thincpropd  49091  functhinclem1  49093  fulltermc  49143  postc  49173
  Copyright terms: Public domain W3C validator