Theorem 2ralbidva 3206

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396   ∈ wcel 2106  ∀wral 3060

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913

This theorem depends on definitions:  df-bi 206  df-an 397  df-ral 3061

This theorem is referenced by:  disjxun  5108  reu3op  6249  opreu2reurex  6251  isocnv3  7282  isotr  7286  f1oweALT  7910  fnmpoovd  8024  pospropd  18230  tosso  18322  isipodrs  18440  mndpropd  18595  mhmpropd  18622  efgred  19544  cmnpropd  19587  ringpropd  20020  lmodprop2d  20441  lsspropd  20535  islmhm2  20556  lmhmpropd  20591  islindf4  21281  assapropd  21312  scmatmats  21897  cpmatel2  22099  1elcpmat  22101  m2cpminvid2  22141  decpmataa0  22154  pmatcollpw2lem  22163  connsub  22809  hausdiag  23033  ist0-4  23117  ismet2  23723  txmetcnp  23940  txmetcn  23941  metuel2  23958  metucn  23964  isngp3  23991  nlmvscn  24088  isclmp  24497  isncvsngp  24550  ipcn  24647  iscfil2  24667  caucfil  24684  cfilresi  24696  ulmdvlem3  25798  cxpcn3  26138  tgjustf  27478  tgjustr  27479  tgcgr4  27536  perpcom  27718  brbtwn2  27917  colinearalglem2  27919  eengtrkg  27998  isarchi2  32091  elmrsubrn  34201  isbnd3b  36317  iscvlat2N  37859  ishlat3N  37889  gicabl  41484  isdomn3  41589  mgmpropd  46189  mgmhmpropd  46199  lidlmmgm  46343  lindslinindsimp2  46664  joindm3  47122  meetdm3  47124  functhinclem1  47181  postc  47222