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

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

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 3046

This theorem is referenced by:  disjxun  5108  reu3op  6268  opreu2reurex  6270  isocnv3  7310  isotr  7314  f1oweALT  7954  fnmpoovd  8069  pospropd  18293  tosso  18385  isipodrs  18503  mgmpropd  18585  mgmhmpropd  18632  sgrppropd  18665  mndpropd  18693  mhmpropd  18726  efgred  19685  cmnpropd  19728  rngpropd  20090  ringpropd  20204  isdomn3  20631  lmodprop2d  20837  lsspropd  20931  islmhm2  20952  lmhmpropd  20987  islindf4  21754  assapropd  21788  scmatmats  22405  cpmatel2  22607  1elcpmat  22609  m2cpminvid2  22649  decpmataa0  22662  pmatcollpw2lem  22671  connsub  23315  hausdiag  23539  ist0-4  23623  ismet2  24228  txmetcnp  24442  txmetcn  24443  metuel2  24460  metucn  24466  isngp3  24493  nlmvscn  24582  isclmp  25004  isncvsngp  25056  ipcn  25153  iscfil2  25173  caucfil  25190  cfilresi  25202  ulmdvlem3  26318  cxpcn3  26665  tgjustf  28407  tgjustr  28408  tgcgr4  28465  perpcom  28647  brbtwn2  28839  colinearalglem2  28841  eengtrkg  28920  isarchi2  33146  opprlidlabs  33463  elmrsubrn  35514  isbnd3b  37786  iscvlat2N  39324  ishlat3N  39354  gicabl  43095  lindslinindsimp2  48456  joindm3  48961  meetdm3  48963  fucofulem2  49304  thincpropd  49435  functhinclem1  49437  fulltermc  49504  postc  49562  islmd  49658  iscmd  49659