Theorem 2ralbidva 3196

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∈ wcel 2113  ∀wral 3049

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 1911

This theorem depends on definitions:  df-bi 207  df-an 396  df-ral 3050

This theorem is referenced by:  disjxun  5094  reu3op  6248  opreu2reurex  6250  isocnv3  7276  isotr  7280  f1oweALT  7914  fnmpoovd  8027  pospropd  18246  tosso  18338  isipodrs  18458  mgmpropd  18574  mgmhmpropd  18621  sgrppropd  18654  mndpropd  18682  mhmpropd  18715  efgred  19675  cmnpropd  19718  rngpropd  20107  ringpropd  20221  isdomn3  20646  lmodprop2d  20873  lsspropd  20967  islmhm2  20988  lmhmpropd  21023  islindf4  21791  assapropd  21825  scmatmats  22453  cpmatel2  22655  1elcpmat  22657  m2cpminvid2  22697  decpmataa0  22710  pmatcollpw2lem  22719  connsub  23363  hausdiag  23587  ist0-4  23671  ismet2  24275  txmetcnp  24489  txmetcn  24490  metuel2  24507  metucn  24513  isngp3  24540  nlmvscn  24629  isclmp  25051  isncvsngp  25103  ipcn  25200  iscfil2  25220  caucfil  25237  cfilresi  25249  ulmdvlem3  26365  cxpcn3  26712  tgjustf  28494  tgjustr  28495  tgcgr4  28552  perpcom  28734  brbtwn2  28927  colinearalglem2  28929  eengtrkg  29008  isarchi2  33216  opprlidlabs  33515  elmrsubrn  35663  isbnd3b  37925  iscvlat2N  39523  ishlat3N  39553  gicabl  43283  lindslinindsimp2  48651  joindm3  49156  meetdm3  49158  fucofulem2  49498  thincpropd  49629  functhinclem1  49631  fulltermc  49698  postc  49756  islmd  49852  iscmd  49853