Theorem 2ralbidva 3191

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

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

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 3045

This theorem is referenced by:  disjxun  5090  reu3op  6240  opreu2reurex  6242  isocnv3  7269  isotr  7273  f1oweALT  7907  fnmpoovd  8020  pospropd  18231  tosso  18323  isipodrs  18443  mgmpropd  18525  mgmhmpropd  18572  sgrppropd  18605  mndpropd  18633  mhmpropd  18666  efgred  19627  cmnpropd  19670  rngpropd  20059  ringpropd  20173  isdomn3  20600  lmodprop2d  20827  lsspropd  20921  islmhm2  20942  lmhmpropd  20977  islindf4  21745  assapropd  21779  scmatmats  22396  cpmatel2  22598  1elcpmat  22600  m2cpminvid2  22640  decpmataa0  22653  pmatcollpw2lem  22662  connsub  23306  hausdiag  23530  ist0-4  23614  ismet2  24219  txmetcnp  24433  txmetcn  24434  metuel2  24451  metucn  24457  isngp3  24484  nlmvscn  24573  isclmp  24995  isncvsngp  25047  ipcn  25144  iscfil2  25164  caucfil  25181  cfilresi  25193  ulmdvlem3  26309  cxpcn3  26656  tgjustf  28418  tgjustr  28419  tgcgr4  28476  perpcom  28658  brbtwn2  28850  colinearalglem2  28852  eengtrkg  28931  isarchi2  33128  opprlidlabs  33423  elmrsubrn  35503  isbnd3b  37775  iscvlat2N  39313  ishlat3N  39343  gicabl  43082  lindslinindsimp2  48458  joindm3  48963  meetdm3  48965  fucofulem2  49306  thincpropd  49437  functhinclem1  49439  fulltermc  49506  postc  49564  islmd  49660  iscmd  49661