Theorem 2ralbidva 2971

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

Syntax hints:   → wi 4   ↔ wb 195   ∧ wa 383   ∈ wcel 1977  ∀wral 2896

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827

This theorem depends on definitions:  df-bi 196  df-an 385  df-ral 2901

This theorem is referenced by:  disjxun  4581  isocnv3  6482  isotr  6486  f1oweALT  7043  fnmpt2ovd  7139  tosso  16859  pospropd  16957  isipodrs  16984  mndpropd  17139  mhmpropd  17164  efgred  17984  cmnpropd  18025  ringpropd  18405  lmodprop2d  18748  lsspropd  18838  islmhm2  18859  lmhmpropd  18894  assapropd  19148  islindf4  19996  scmatmats  20136  cpmatel2  20337  1elcpmat  20339  m2cpminvid2  20379  decpmataa0  20392  pmatcollpw2lem  20401  connsub  21034  hausdiag  21258  ist0-4  21342  ismet2  21948  txmetcnp  22162  txmetcn  22163  metuel2  22180  metucn  22186  isngp3  22212  nlmvscn  22301  isclmp  22705  isncvsngp  22757  ipcn  22853  iscfil2  22872  caucfil  22889  cfilresi  22901  ulmdvlem3  23960  cxpcn3  24289  tgcgr4  25226  perpcom  25408  brbtwn2  25585  colinearalglem2  25587  eengtrkg  25665  isarchi2  29070  elmrsubrn  30671  isbnd3b  32754  iscvlat2N  33629  ishlat3N  33659  gicabl  36687  isdomn3  36801  mgmpropd  41565  mgmhmpropd  41575  lidlmmgm  41715  lindslinindsimp2  42046