Theorem 2ralbidva 3197

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 3154	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (∀𝑦 ∈ 𝐵 𝜓 ↔ ∀𝑦 ∈ 𝐵 𝜒))
4	3	ralbidva 3154	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  5100  reu3op  6253  opreu2reurex  6255  isocnv3  7289  isotr  7293  f1oweALT  7930  fnmpoovd  8043  pospropd  18266  tosso  18358  isipodrs  18478  mgmpropd  18560  mgmhmpropd  18607  sgrppropd  18640  mndpropd  18668  mhmpropd  18701  efgred  19662  cmnpropd  19705  rngpropd  20094  ringpropd  20208  isdomn3  20635  lmodprop2d  20862  lsspropd  20956  islmhm2  20977  lmhmpropd  21012  islindf4  21780  assapropd  21814  scmatmats  22431  cpmatel2  22633  1elcpmat  22635  m2cpminvid2  22675  decpmataa0  22688  pmatcollpw2lem  22697  connsub  23341  hausdiag  23565  ist0-4  23649  ismet2  24254  txmetcnp  24468  txmetcn  24469  metuel2  24486  metucn  24492  isngp3  24519  nlmvscn  24608  isclmp  25030  isncvsngp  25082  ipcn  25179  iscfil2  25199  caucfil  25216  cfilresi  25228  ulmdvlem3  26344  cxpcn3  26691  tgjustf  28453  tgjustr  28454  tgcgr4  28511  perpcom  28693  brbtwn2  28885  colinearalglem2  28887  eengtrkg  28966  isarchi2  33154  opprlidlabs  33449  elmrsubrn  35500  isbnd3b  37772  iscvlat2N  39310  ishlat3N  39340  gicabl  43081  lindslinindsimp2  48445  joindm3  48950  meetdm3  48952  fucofulem2  49293  thincpropd  49424  functhinclem1  49426  fulltermc  49493  postc  49551  islmd  49647  iscmd  49648