Theorem 2ralbidva 3226

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

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 399   ∈ wcel 2144  ∀wral 3078

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-5 1932

This theorem depends on definitions:  df-bi 209  df-an 400  df-ral 3079

This theorem is referenced by:  disjxun  5100  reu3op  6281  opreu2reurex  6283  isocnv3  7318  isotr  7322  f1oweALT  7955  fnmpoovd  8068  pospropd  18359  tosso  18451  isipodrs  18571  mgmpropd  18687  mgmhmpropd  18734  sgrppropd  18767  mndpropd  18795  mhmpropd  18828  efgred  19790  cmnpropd  19833  rngpropd  20222  ringpropd  20340  isdomn3  20767  lmodprop2d  20993  lsspropd  21086  islmhm2  21107  lmhmpropd  21142  islindf4  21892  assapropd  21925  scmatmats  22573  cpmatel2  22775  1elcpmat  22777  m2cpminvid2  22817  decpmataa0  22830  pmatcollpw2lem  22839  connsub  23483  hausdiag  23707  ist0-4  23791  ismet2  24395  txmetcnp  24609  txmetcn  24610  metuel2  24627  metucn  24633  isngp3  24660  nlmvscn  24749  isclmp  25161  isncvsngp  25213  ipcn  25310  iscfil2  25330  caucfil  25347  cfilresi  25359  ulmdvlem3  26467  cxpcn3  26815  tgjustf  28644  tgjustr  28645  tgcgr4  28702  perpcom  28888  brbtwn2  29108  colinearalglem2  29110  eengtrkg  29189  isarchi2  33367  opprlidlabs  33675  elmrsubrn  35875  nmulprop  36545  nmulcom  36549  isbnd3b  38289  iscvlat2N  39953  ishlat3N  39983  gicabl  43681  lindslinindsimp2  49090  joindm3  49595  meetdm3  49597  fucofulem2  49937  thincpropd  50068  functhinclem1  50070  fulltermc  50137  postc  50195  islmd  50291  iscmd  50292