Theorem 2ralbidva 3219

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910

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

This theorem is referenced by:  disjxun  5141  reu3op  6312  opreu2reurex  6314  isocnv3  7352  isotr  7356  f1oweALT  7997  fnmpoovd  8112  pospropd  18372  tosso  18464  isipodrs  18582  mgmpropd  18664  mgmhmpropd  18711  sgrppropd  18744  mndpropd  18772  mhmpropd  18805  efgred  19766  cmnpropd  19809  rngpropd  20171  ringpropd  20285  isdomn3  20715  lmodprop2d  20922  lsspropd  21016  islmhm2  21037  lmhmpropd  21072  islindf4  21858  assapropd  21892  scmatmats  22517  cpmatel2  22719  1elcpmat  22721  m2cpminvid2  22761  decpmataa0  22774  pmatcollpw2lem  22783  connsub  23429  hausdiag  23653  ist0-4  23737  ismet2  24343  txmetcnp  24560  txmetcn  24561  metuel2  24578  metucn  24584  isngp3  24611  nlmvscn  24708  isclmp  25130  isncvsngp  25183  ipcn  25280  iscfil2  25300  caucfil  25317  cfilresi  25329  ulmdvlem3  26445  cxpcn3  26791  tgjustf  28481  tgjustr  28482  tgcgr4  28539  perpcom  28721  brbtwn2  28920  colinearalglem2  28922  eengtrkg  29001  isarchi2  33192  opprlidlabs  33513  elmrsubrn  35525  isbnd3b  37792  iscvlat2N  39325  ishlat3N  39355  gicabl  43111  lindslinindsimp2  48380  joindm3  48866  meetdm3  48868  fucofulem2  49006  thincpropd  49091  functhinclem1  49093  fulltermc  49143  postc  49173