Theorem 2ralbidva 3206

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 468	. . 3 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) → (𝜓 ↔ 𝜒))
3	2	ralbidva 3168	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (∀𝑦 ∈ 𝐵 𝜓 ↔ ∀𝑦 ∈ 𝐵 𝜒))
4	3	ralbidva 3168	1 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜒))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396   ∈ wcel 2105  ∀wral 3061

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912

This theorem depends on definitions:  df-bi 206  df-an 397  df-ral 3062

This theorem is referenced by:  disjxun  5090  reu3op  6230  opreu2reurex  6232  isocnv3  7259  isotr  7263  f1oweALT  7883  fnmpoovd  7995  pospropd  18142  tosso  18234  isipodrs  18352  mndpropd  18507  mhmpropd  18533  efgred  19449  cmnpropd  19491  ringpropd  19916  lmodprop2d  20291  lsspropd  20385  islmhm2  20406  lmhmpropd  20441  islindf4  21151  assapropd  21182  scmatmats  21766  cpmatel2  21968  1elcpmat  21970  m2cpminvid2  22010  decpmataa0  22023  pmatcollpw2lem  22032  connsub  22678  hausdiag  22902  ist0-4  22986  ismet2  23592  txmetcnp  23809  txmetcn  23810  metuel2  23827  metucn  23833  isngp3  23860  nlmvscn  23957  isclmp  24366  isncvsngp  24419  ipcn  24516  iscfil2  24536  caucfil  24553  cfilresi  24565  ulmdvlem3  25667  cxpcn3  26007  tgjustf  27123  tgjustr  27124  tgcgr4  27181  perpcom  27363  brbtwn2  27562  colinearalglem2  27564  eengtrkg  27643  isarchi2  31726  elmrsubrn  33781  isbnd3b  36056  iscvlat2N  37599  ishlat3N  37629  gicabl  41195  isdomn3  41300  mgmpropd  45688  mgmhmpropd  45698  lidlmmgm  45842  lindslinindsimp2  46163  joindm3  46622  meetdm3  46624  functhinclem1  46681  postc  46722