Theorem 2ralbidva 3233

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

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400   ∈ wcel 2149  ∀wral 3085

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937

This theorem depends on definitions:  df-bi 210  df-an 401  df-ral 3086

This theorem is referenced by:  disjxun  5111  reu3op  6294  opreu2reurex  6296  isocnv3  7331  isotr  7335  f1oweALT  7969  fnmpoovd  8082  pospropd  18381  tosso  18473  isipodrs  18593  mgmpropd  18709  mgmhmpropd  18756  sgrppropd  18789  mndpropd  18817  mhmpropd  18850  efgred  19818  cmnpropd  19861  rngpropd  20252  ringpropd  20371  isdomn3  20799  lmodprop2d  21023  lsspropd  21116  islmhm2  21137  lmhmpropd  21172  df2idl2crng  21392  islindf4  21957  assapropd  21990  scmatmats  22637  cpmatel2  22839  1elcpmat  22841  m2cpminvid2  22881  decpmataa0  22894  pmatcollpw2lem  22903  connsub  23547  hausdiag  23771  ist0-4  23855  ismet2  24459  txmetcnp  24673  txmetcn  24674  metuel2  24691  metucn  24697  isngp3  24724  nlmvscn  24813  isclmp  25225  isncvsngp  25277  ipcn  25374  iscfil2  25394  caucfil  25411  cfilresi  25423  ulmdvlem3  26531  cxpcn3  26879  tgjustf  28708  tgjustr  28709  tgcgr4  28766  perpcom  28952  brbtwn2  29196  colinearalglem2  29198  eengtrkg  29277  isarchi2  33446  opprlidlabs  33712  elmrsubrn  35945  nmulprop  36615  nmulcom  36619  isbnd3b  38358  iscvlat2N  40022  ishlat3N  40052  gicabl  43752  lindslinindsimp2  49162  joindm3  49666  meetdm3  49668  fucofulem2  50008  thincpropd  50139  functhinclem1  50141  fulltermc  50208  postc  50266  islmd  50362  iscmd  50363