Theorem 2ralbidva 3224

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   ∈ wcel 2145  ∀wral 3076

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943

This proof depends on definitions:  df-bi 210  df-an 402  df-ral 3077

This theorem is used by:  disjxun  5101  reu3op  6292  opreu2reurex  6294  isocnv3  7336  isotr  7340  f1oweALT  7975  fnmpoovd  8089  pospropd  18438  tosso  18530  isipodrs  18650  mgmpropd  18768  mgmhmpropd  18826  sgrppropd  18859  mndpropd  18890  mhmpropd  18926  efgred  19901  cmnpropd  19944  rngpropd  20335  ringpropd  20458  isdomn3  20905  lmodprop2d  21138  lsspropd  21231  islmhm2  21252  lmhmpropd  21287  df2idl2crng  21516  islindf4  22083  assapropd  22118  scmatmats  22765  cpmatel2  22970  1elcpmat  22972  m2cpminvid2  23012  decpmataa0  23025  pmatcollpw2lem  23034  connsub  23678  hausdiag  23903  ist0-4  23987  ismet2  24591  txmetcnp  24805  txmetcn  24806  metuel2  24823  metucn  24829  isngp3  24856  nlmvscn  24945  isclmp  25357  isncvsngp  25409  ipcn  25506  iscfil2  25526  caucfil  25543  cfilresi  25555  ulmdvlem3  26670  cxpcn3  27017  tgjustf  28846  tgjustr  28847  tgcgr4  28905  perpcom  29099  brbtwn2  29394  colinearalglem2  29396  eengtrkg  29475  isarchi2  33657  opprlidlabs  33920  elmrsubrn  36182  nmulprop  36837  nmulcom  36841  nadddilem2  36868  nadddilem4  36870  isbnd3b  38600  iscvlat2N  40262  ishlat3N  40292  gicabl  44005  lindslinindsimp2  49458  joindm3  49960  meetdm3  49962  fucofulem2  50302  thincpropd  50433  functhinclem1  50435  fulltermc  50502  postc  50560  islmd  50656  iscmd  50657