Theorem 2ralbidva 3194

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911

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

This theorem is referenced by:  disjxun  5087  reu3op  6239  opreu2reurex  6241  isocnv3  7266  isotr  7270  f1oweALT  7904  fnmpoovd  8017  pospropd  18231  tosso  18323  isipodrs  18443  mgmpropd  18559  mgmhmpropd  18606  sgrppropd  18639  mndpropd  18667  mhmpropd  18700  efgred  19660  cmnpropd  19703  rngpropd  20092  ringpropd  20206  isdomn3  20630  lmodprop2d  20857  lsspropd  20951  islmhm2  20972  lmhmpropd  21007  islindf4  21775  assapropd  21809  scmatmats  22426  cpmatel2  22628  1elcpmat  22630  m2cpminvid2  22670  decpmataa0  22683  pmatcollpw2lem  22692  connsub  23336  hausdiag  23560  ist0-4  23644  ismet2  24248  txmetcnp  24462  txmetcn  24463  metuel2  24480  metucn  24486  isngp3  24513  nlmvscn  24602  isclmp  25024  isncvsngp  25076  ipcn  25173  iscfil2  25193  caucfil  25210  cfilresi  25222  ulmdvlem3  26338  cxpcn3  26685  tgjustf  28451  tgjustr  28452  tgcgr4  28509  perpcom  28691  brbtwn2  28883  colinearalglem2  28885  eengtrkg  28964  isarchi2  33154  opprlidlabs  33450  elmrsubrn  35564  isbnd3b  37824  iscvlat2N  39422  ishlat3N  39452  gicabl  43191  lindslinindsimp2  48563  joindm3  49068  meetdm3  49070  fucofulem2  49411  thincpropd  49542  functhinclem1  49544  fulltermc  49611  postc  49669  islmd  49765  iscmd  49766