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

Theorem 2ralbidva 3195
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 3193 . 2 ((𝜑𝑥𝐴) → (∀𝑦𝐵 𝜓 ↔ ∀𝑦𝐵 𝜒))
43ralbidva 3193 1 (𝜑 → (∀𝑥𝐴𝑦𝐵 𝜓 ↔ ∀𝑥𝐴𝑦𝐵 𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207  wa 396  wcel 2105  wral 3135
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 3140
This theorem is referenced by:  disjxun  5055  reu3op  6136  opreu2reurex  6138  isocnv3  7074  isotr  7078  f1oweALT  7662  fnmpoovd  7771  tosso  17634  pospropd  17732  isipodrs  17759  mndpropd  17924  mhmpropd  17950  efgred  18803  cmnpropd  18845  ringpropd  19261  lmodprop2d  19625  lsspropd  19718  islmhm2  19739  lmhmpropd  19774  assapropd  20029  islindf4  20910  scmatmats  21048  cpmatel2  21249  1elcpmat  21251  m2cpminvid2  21291  decpmataa0  21304  pmatcollpw2lem  21313  connsub  21957  hausdiag  22181  ist0-4  22265  ismet2  22870  txmetcnp  23084  txmetcn  23085  metuel2  23102  metucn  23108  isngp3  23134  nlmvscn  23223  isclmp  23628  isncvsngp  23680  ipcn  23776  iscfil2  23796  caucfil  23813  cfilresi  23825  ulmdvlem3  24917  cxpcn3  25256  tgjustf  26186  tgjustr  26187  tgcgr4  26244  perpcom  26426  brbtwn2  26618  colinearalglem2  26620  eengtrkg  26699  isarchi2  30741  elmrsubrn  32664  isbnd3b  34944  iscvlat2N  36340  ishlat3N  36370  gicabl  39577  isdomn3  39682  mgmpropd  43919  mgmhmpropd  43929  lidlmmgm  44124  lindslinindsimp2  44446
  Copyright terms: Public domain W3C validator