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

Theorem 2ralbidva 3137
Description: Formula-building rule for restricted universal quantifiers (deduction rule). (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 458 . . 3 (((𝜑𝑥𝐴) ∧ 𝑦𝐵) → (𝜓𝜒))
32ralbidva 3134 . 2 ((𝜑𝑥𝐴) → (∀𝑦𝐵 𝜓 ↔ ∀𝑦𝐵 𝜒))
43ralbidva 3134 1 (𝜑 → (∀𝑥𝐴𝑦𝐵 𝜓 ↔ ∀𝑥𝐴𝑦𝐵 𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 382  wcel 2145  wral 3061
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991
This theorem depends on definitions:  df-bi 197  df-an 383  df-ral 3066
This theorem is referenced by:  disjxun  4784  isocnv3  6725  isotr  6729  f1oweALT  7299  fnmpt2ovd  7402  fnmpt2ovdOLD  7403  tosso  17244  pospropd  17342  isipodrs  17369  mndpropd  17524  mhmpropd  17549  efgred  18368  cmnpropd  18409  ringpropd  18790  lmodprop2d  19135  lsspropd  19230  islmhm2  19251  lmhmpropd  19286  assapropd  19542  islindf4  20394  scmatmats  20535  cpmatel2  20738  1elcpmat  20740  m2cpminvid2  20780  decpmataa0  20793  pmatcollpw2lem  20802  connsub  21445  hausdiag  21669  ist0-4  21753  ismet2  22358  txmetcnp  22572  txmetcn  22573  metuel2  22590  metucn  22596  isngp3  22622  nlmvscn  22711  isclmp  23116  isncvsngp  23168  ipcn  23264  iscfil2  23283  caucfil  23300  cfilresi  23312  ulmdvlem3  24376  cxpcn3  24710  tgcgr4  25647  perpcom  25829  brbtwn2  26006  colinearalglem2  26008  eengtrkg  26086  isarchi2  30079  elmrsubrn  31755  isbnd3b  33916  iscvlat2N  35133  ishlat3N  35163  gicabl  38195  isdomn3  38308  mgmpropd  42303  mgmhmpropd  42313  lidlmmgm  42453  lindslinindsimp2  42780
  Copyright terms: Public domain W3C validator