Theorem 2ralbidva 3216

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907

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

This theorem is referenced by:  disjxun  5145  reu3op  6313  opreu2reurex  6315  isocnv3  7351  isotr  7355  f1oweALT  7995  fnmpoovd  8110  pospropd  18384  tosso  18476  isipodrs  18594  mgmpropd  18676  mgmhmpropd  18723  sgrppropd  18756  mndpropd  18784  mhmpropd  18817  efgred  19780  cmnpropd  19823  rngpropd  20191  ringpropd  20301  isdomn3  20731  lmodprop2d  20938  lsspropd  21033  islmhm2  21054  lmhmpropd  21089  islindf4  21875  assapropd  21909  scmatmats  22532  cpmatel2  22734  1elcpmat  22736  m2cpminvid2  22776  decpmataa0  22789  pmatcollpw2lem  22798  connsub  23444  hausdiag  23668  ist0-4  23752  ismet2  24358  txmetcnp  24575  txmetcn  24576  metuel2  24593  metucn  24599  isngp3  24626  nlmvscn  24723  isclmp  25143  isncvsngp  25196  ipcn  25293  iscfil2  25313  caucfil  25330  cfilresi  25342  ulmdvlem3  26459  cxpcn3  26805  tgjustf  28495  tgjustr  28496  tgcgr4  28553  perpcom  28735  brbtwn2  28934  colinearalglem2  28936  eengtrkg  29015  isarchi2  33174  opprlidlabs  33492  elmrsubrn  35504  isbnd3b  37771  iscvlat2N  39305  ishlat3N  39335  gicabl  43087  lindslinindsimp2  48308  joindm3  48765  meetdm3  48767  functhinclem1  48840  postc  48884