Theorem 2ralbidva 3163

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

Step	Hyp	Ref	Expression
1		2ralbidva.1	. . . 4 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → (𝜓 ↔ 𝜒))
2	1	anassrs 471	. . 3 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) → (𝜓 ↔ 𝜒))
3	2	ralbidva 3161	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (∀𝑦 ∈ 𝐵 𝜓 ↔ ∀𝑦 ∈ 𝐵 𝜒))
4	3	ralbidva 3161	1 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜒))

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   ∈ wcel 2111  ∀wral 3106

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 1911

This theorem depends on definitions:  df-bi 210  df-an 400  df-ral 3111

This theorem is referenced by:  disjxun  5028  reu3op  6111  opreu2reurex  6113  isocnv3  7064  isotr  7068  f1oweALT  7655  fnmpoovd  7765  tosso  17638  pospropd  17736  isipodrs  17763  mndpropd  17928  mhmpropd  17954  efgred  18866  cmnpropd  18908  ringpropd  19328  lmodprop2d  19689  lsspropd  19782  islmhm2  19803  lmhmpropd  19838  islindf4  20527  assapropd  20558  scmatmats  21116  cpmatel2  21318  1elcpmat  21320  m2cpminvid2  21360  decpmataa0  21373  pmatcollpw2lem  21382  connsub  22026  hausdiag  22250  ist0-4  22334  ismet2  22940  txmetcnp  23154  txmetcn  23155  metuel2  23172  metucn  23178  isngp3  23204  nlmvscn  23293  isclmp  23702  isncvsngp  23754  ipcn  23850  iscfil2  23870  caucfil  23887  cfilresi  23899  ulmdvlem3  24997  cxpcn3  25337  tgjustf  26267  tgjustr  26268  tgcgr4  26325  perpcom  26507  brbtwn2  26699  colinearalglem2  26701  eengtrkg  26780  isarchi2  30864  elmrsubrn  32880  isbnd3b  35223  iscvlat2N  36620  ishlat3N  36650  gicabl  40043  isdomn3  40148  mgmpropd  44395  mgmhmpropd  44405  lidlmmgm  44549  lindslinindsimp2  44872