Theorem 2ralbidva 2988

Description: Formula-building rule for restricted universal quantifiers (deduction rule). (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 680	. . 3 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) → (𝜓 ↔ 𝜒))
3	2	ralbidva 2985	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (∀𝑦 ∈ 𝐵 𝜓 ↔ ∀𝑦 ∈ 𝐵 𝜒))
4	3	ralbidva 2985	1 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜒))

Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 384   ∈ wcel 1990  ∀wral 2912

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839

This theorem depends on definitions:  df-bi 197  df-an 386  df-ral 2917

This theorem is referenced by:  disjxun  4651  isocnv3  6582  isotr  6586  f1oweALT  7152  fnmpt2ovd  7252  tosso  17036  pospropd  17134  isipodrs  17161  mndpropd  17316  mhmpropd  17341  efgred  18161  cmnpropd  18202  ringpropd  18582  lmodprop2d  18925  lsspropd  19017  islmhm2  19038  lmhmpropd  19073  assapropd  19327  islindf4  20177  scmatmats  20317  cpmatel2  20518  1elcpmat  20520  m2cpminvid2  20560  decpmataa0  20573  pmatcollpw2lem  20582  connsub  21224  hausdiag  21448  ist0-4  21532  ismet2  22138  txmetcnp  22352  txmetcn  22353  metuel2  22370  metucn  22376  isngp3  22402  nlmvscn  22491  isclmp  22897  isncvsngp  22949  ipcn  23045  iscfil2  23064  caucfil  23081  cfilresi  23093  ulmdvlem3  24156  cxpcn3  24489  tgcgr4  25426  perpcom  25608  brbtwn2  25785  colinearalglem2  25787  eengtrkg  25865  isarchi2  29739  elmrsubrn  31417  isbnd3b  33584  iscvlat2N  34611  ishlat3N  34641  gicabl  37669  isdomn3  37782  mgmpropd  41775  mgmhmpropd  41785  lidlmmgm  41925  lindslinindsimp2  42252