Theorem 2ralbidva 3148

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

Syntax hints:   → wi 4   ↔ wb 198   ∧ wa 387   ∈ wcel 2050  ∀wral 3088

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869

This theorem depends on definitions:  df-bi 199  df-an 388  df-ral 3093

This theorem is referenced by:  disjxun  4927  reu3op  5981  opreu2reurex  5983  isocnv3  6908  isotr  6912  f1oweALT  7485  fnmpoovd  7590  tosso  17504  pospropd  17602  isipodrs  17629  mndpropd  17784  mhmpropd  17809  efgred  18634  cmnpropd  18675  ringpropd  19055  lmodprop2d  19418  lsspropd  19511  islmhm2  19532  lmhmpropd  19567  assapropd  19821  islindf4  20684  scmatmats  20824  cpmatel2  21025  1elcpmat  21027  m2cpminvid2  21067  decpmataa0  21080  pmatcollpw2lem  21089  connsub  21733  hausdiag  21957  ist0-4  22041  ismet2  22646  txmetcnp  22860  txmetcn  22861  metuel2  22878  metucn  22884  isngp3  22910  nlmvscn  22999  isclmp  23404  isncvsngp  23456  ipcn  23552  iscfil2  23572  caucfil  23589  cfilresi  23601  ulmdvlem3  24693  cxpcn3  25030  tgjustf  25961  tgjustr  25962  tgcgr4  26019  perpcom  26201  brbtwn2  26394  colinearalglem2  26396  eengtrkg  26475  isarchi2  30486  elmrsubrn  32293  isbnd3b  34511  iscvlat2N  35911  ishlat3N  35941  gicabl  39101  isdomn3  39206  mgmpropd  43416  mgmhmpropd  43426  lidlmmgm  43566  lindslinindsimp2  43891