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

Theorem 2ralbidva 3198
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 468 . . 3 (((𝜑𝑥𝐴) ∧ 𝑦𝐵) → (𝜓𝜒))
32ralbidva 3196 . 2 ((𝜑𝑥𝐴) → (∀𝑦𝐵 𝜓 ↔ ∀𝑦𝐵 𝜒))
43ralbidva 3196 1 (𝜑 → (∀𝑥𝐴𝑦𝐵 𝜓 ↔ ∀𝑥𝐴𝑦𝐵 𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207  wa 396  wcel 2105  wral 3138
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902
This theorem depends on definitions:  df-bi 208  df-an 397  df-ral 3143
This theorem is referenced by:  disjxun  5056  reu3op  6137  opreu2reurex  6139  isocnv3  7074  isotr  7078  f1oweALT  7664  fnmpoovd  7773  tosso  17636  pospropd  17734  isipodrs  17761  mndpropd  17926  mhmpropd  17952  efgred  18805  cmnpropd  18847  ringpropd  19263  lmodprop2d  19627  lsspropd  19720  islmhm2  19741  lmhmpropd  19776  assapropd  20031  islindf4  20912  scmatmats  21050  cpmatel2  21251  1elcpmat  21253  m2cpminvid2  21293  decpmataa0  21306  pmatcollpw2lem  21315  connsub  21959  hausdiag  22183  ist0-4  22267  ismet2  22872  txmetcnp  23086  txmetcn  23087  metuel2  23104  metucn  23110  isngp3  23136  nlmvscn  23225  isclmp  23630  isncvsngp  23682  ipcn  23778  iscfil2  23798  caucfil  23815  cfilresi  23827  ulmdvlem3  24919  cxpcn3  25256  tgjustf  26187  tgjustr  26188  tgcgr4  26245  perpcom  26427  brbtwn2  26619  colinearalglem2  26621  eengtrkg  26700  isarchi2  30742  elmrsubrn  32665  isbnd3b  34946  iscvlat2N  36342  ishlat3N  36372  gicabl  39579  isdomn3  39684  mgmpropd  43889  mgmhmpropd  43899  lidlmmgm  44094  lindslinindsimp2  44416
  Copyright terms: Public domain W3C validator