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

Theorem 2ralbidva 3193
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 471 . . 3 (((𝜑𝑥𝐴) ∧ 𝑦𝐵) → (𝜓𝜒))
32ralbidva 3191 . 2 ((𝜑𝑥𝐴) → (∀𝑦𝐵 𝜓 ↔ ∀𝑦𝐵 𝜒))
43ralbidva 3191 1 (𝜑 → (∀𝑥𝐴𝑦𝐵 𝜓 ↔ ∀𝑥𝐴𝑦𝐵 𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  wa 399  wcel 2115  wral 3133
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912
This theorem depends on definitions:  df-bi 210  df-an 400  df-ral 3138
This theorem is referenced by:  disjxun  5050  reu3op  6130  opreu2reurex  6132  isocnv3  7078  isotr  7082  f1oweALT  7668  fnmpoovd  7778  tosso  17646  pospropd  17744  isipodrs  17771  mndpropd  17936  mhmpropd  17962  efgred  18874  cmnpropd  18916  ringpropd  19335  lmodprop2d  19696  lsspropd  19789  islmhm2  19810  lmhmpropd  19845  assapropd  20101  islindf4  20982  scmatmats  21120  cpmatel2  21321  1elcpmat  21323  m2cpminvid2  21363  decpmataa0  21376  pmatcollpw2lem  21385  connsub  22029  hausdiag  22253  ist0-4  22337  ismet2  22943  txmetcnp  23157  txmetcn  23158  metuel2  23175  metucn  23181  isngp3  23207  nlmvscn  23296  isclmp  23705  isncvsngp  23757  ipcn  23853  iscfil2  23873  caucfil  23890  cfilresi  23902  ulmdvlem3  25000  cxpcn3  25340  tgjustf  26270  tgjustr  26271  tgcgr4  26328  perpcom  26510  brbtwn2  26702  colinearalglem2  26704  eengtrkg  26783  isarchi2  30846  elmrsubrn  32824  isbnd3b  35168  iscvlat2N  36565  ishlat3N  36595  gicabl  39959  isdomn3  40064  mgmpropd  44321  mgmhmpropd  44331  lidlmmgm  44475  lindslinindsimp2  44798
  Copyright terms: Public domain W3C validator