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  5084  reu3op  6252  opreu2reurex  6254  isocnv3  7282  isotr  7286  f1oweALT  7920  fnmpoovd  8032  pospropd  18286  tosso  18378  isipodrs  18498  mgmpropd  18614  mgmhmpropd  18661  sgrppropd  18694  mndpropd  18722  mhmpropd  18755  efgred  19718  cmnpropd  19761  rngpropd  20150  ringpropd  20264  isdomn3  20687  lmodprop2d  20914  lsspropd  21008  islmhm2  21029  lmhmpropd  21064  islindf4  21832  assapropd  21865  scmatmats  22490  cpmatel2  22692  1elcpmat  22694  m2cpminvid2  22734  decpmataa0  22747  pmatcollpw2lem  22756  connsub  23400  hausdiag  23624  ist0-4  23708  ismet2  24312  txmetcnp  24526  txmetcn  24527  metuel2  24544  metucn  24550  isngp3  24577  nlmvscn  24666  isclmp  25078  isncvsngp  25130  ipcn  25227  iscfil2  25247  caucfil  25264  cfilresi  25276  ulmdvlem3  26384  cxpcn3  26729  tgjustf  28559  tgjustr  28560  tgcgr4  28617  perpcom  28799  brbtwn2  28992  colinearalglem2  28994  eengtrkg  29073  isarchi2  33265  opprlidlabs  33564  elmrsubrn  35722  isbnd3b  38124  iscvlat2N  39788  ishlat3N  39818  gicabl  43549  lindslinindsimp2  48955  joindm3  49460  meetdm3  49462  fucofulem2  49802  thincpropd  49933  functhinclem1  49935  fulltermc  50002  postc  50060  islmd  50156  iscmd  50157