Theorem 2ralbidva 3126

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

Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 383   ∈ wcel 2139  ∀wral 3050

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988

This theorem depends on definitions:  df-bi 197  df-an 385  df-ral 3055

This theorem is referenced by:  disjxun  4802  isocnv3  6745  isotr  6749  f1oweALT  7317  fnmpt2ovd  7420  tosso  17237  pospropd  17335  isipodrs  17362  mndpropd  17517  mhmpropd  17542  efgred  18361  cmnpropd  18402  ringpropd  18782  lmodprop2d  19127  lsspropd  19219  islmhm2  19240  lmhmpropd  19275  assapropd  19529  islindf4  20379  scmatmats  20519  cpmatel2  20720  1elcpmat  20722  m2cpminvid2  20762  decpmataa0  20775  pmatcollpw2lem  20784  connsub  21426  hausdiag  21650  ist0-4  21734  ismet2  22339  txmetcnp  22553  txmetcn  22554  metuel2  22571  metucn  22577  isngp3  22603  nlmvscn  22692  isclmp  23097  isncvsngp  23149  ipcn  23245  iscfil2  23264  caucfil  23281  cfilresi  23293  ulmdvlem3  24355  cxpcn3  24688  tgcgr4  25625  perpcom  25807  brbtwn2  25984  colinearalglem2  25986  eengtrkg  26064  isarchi2  30048  elmrsubrn  31724  isbnd3b  33897  iscvlat2N  35114  ishlat3N  35144  gicabl  38171  isdomn3  38284  mgmpropd  42285  mgmhmpropd  42295  lidlmmgm  42435  lindslinindsimp2  42762