Theorem 2ralbidva 3200

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

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

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 3053

This theorem is referenced by:  disjxun  5098  reu3op  6260  opreu2reurex  6262  isocnv3  7290  isotr  7294  f1oweALT  7928  fnmpoovd  8041  pospropd  18262  tosso  18354  isipodrs  18474  mgmpropd  18590  mgmhmpropd  18637  sgrppropd  18670  mndpropd  18698  mhmpropd  18731  efgred  19694  cmnpropd  19737  rngpropd  20126  ringpropd  20240  isdomn3  20665  lmodprop2d  20892  lsspropd  20986  islmhm2  21007  lmhmpropd  21042  islindf4  21810  assapropd  21844  scmatmats  22472  cpmatel2  22674  1elcpmat  22676  m2cpminvid2  22716  decpmataa0  22729  pmatcollpw2lem  22738  connsub  23382  hausdiag  23606  ist0-4  23690  ismet2  24294  txmetcnp  24508  txmetcn  24509  metuel2  24526  metucn  24532  isngp3  24559  nlmvscn  24648  isclmp  25070  isncvsngp  25122  ipcn  25219  iscfil2  25239  caucfil  25256  cfilresi  25268  ulmdvlem3  26384  cxpcn3  26731  tgjustf  28563  tgjustr  28564  tgcgr4  28621  perpcom  28803  brbtwn2  28996  colinearalglem2  28998  eengtrkg  29077  isarchi2  33285  opprlidlabs  33584  elmrsubrn  35742  isbnd3b  38065  iscvlat2N  39729  ishlat3N  39759  gicabl  43485  lindslinindsimp2  48852  joindm3  49357  meetdm3  49359  fucofulem2  49699  thincpropd  49830  functhinclem1  49832  fulltermc  49899  postc  49957  islmd  50053  iscmd  50054