Theorem 2ralbidva 3199

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

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

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 1912

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

This theorem is referenced by:  disjxun  5083  reu3op  6256  opreu2reurex  6258  isocnv3  7287  isotr  7291  f1oweALT  7925  fnmpoovd  8037  pospropd  18291  tosso  18383  isipodrs  18503  mgmpropd  18619  mgmhmpropd  18666  sgrppropd  18699  mndpropd  18727  mhmpropd  18760  efgred  19723  cmnpropd  19766  rngpropd  20155  ringpropd  20269  isdomn3  20692  lmodprop2d  20919  lsspropd  21012  islmhm2  21033  lmhmpropd  21068  islindf4  21818  assapropd  21851  scmatmats  22476  cpmatel2  22678  1elcpmat  22680  m2cpminvid2  22720  decpmataa0  22733  pmatcollpw2lem  22742  connsub  23386  hausdiag  23610  ist0-4  23694  ismet2  24298  txmetcnp  24512  txmetcn  24513  metuel2  24530  metucn  24536  isngp3  24563  nlmvscn  24652  isclmp  25064  isncvsngp  25116  ipcn  25213  iscfil2  25233  caucfil  25250  cfilresi  25262  ulmdvlem3  26367  cxpcn3  26712  tgjustf  28541  tgjustr  28542  tgcgr4  28599  perpcom  28781  brbtwn2  28974  colinearalglem2  28976  eengtrkg  29055  isarchi2  33246  opprlidlabs  33545  elmrsubrn  35702  isbnd3b  38106  iscvlat2N  39770  ishlat3N  39800  gicabl  43527  lindslinindsimp2  48939  joindm3  49444  meetdm3  49446  fucofulem2  49786  thincpropd  49917  functhinclem1  49919  fulltermc  49986  postc  50044  islmd  50140  iscmd  50141