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 2144  ∀wral 3076

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942

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

This theorem is used by:  disjxun  5100  reu3op  6295  opreu2reurex  6297  isocnv3  7340  isotr  7344  f1oweALT  7984  fnmpoovd  8098  pospropd  18499  tosso  18591  isipodrs  18711  mgmpropd  18829  mgmhmpropd  18887  sgrppropd  18920  mndpropd  18951  mhmpropd  18987  efgred  19962  cmnpropd  20005  rngpropd  20396  ringpropd  20519  isdomn3  20966  lmodprop2d  21199  lsspropd  21292  islmhm2  21313  lmhmpropd  21348  df2idl2crng  21577  islindf4  22144  assapropd  22179  scmatmats  22826  cpmatel2  23031  1elcpmat  23033  m2cpminvid2  23073  decpmataa0  23086  pmatcollpw2lem  23095  connsub  23739  hausdiag  23964  ist0-4  24048  ismet2  24652  txmetcnp  24866  txmetcn  24867  metuel2  24884  metucn  24890  isngp3  24917  nlmvscn  25006  isclmp  25418  isncvsngp  25470  ipcn  25567  iscfil2  25587  caucfil  25604  cfilresi  25616  ulmdvlem3  26729  cxpcn3  27076  tgjustf  28935  tgjustr  28936  tgcgr4  28994  perpcom  29188  brbtwn2  29483  colinearalglem2  29485  eengtrkg  29564  isarchi2  33746  opprlidlabs  34009  elmrsubrn  36285  nmulprop  36939  nmulcom  36943  nadddilem2  36970  nadddilem4  36972  isbnd3b  38720  iscvlat2N  40382  ishlat3N  40412  gicabl  44101  lindslinindsimp2  49575  joindm3  50077  meetdm3  50079  fucofulem2  50419  thincpropd  50550  functhinclem1  50552  fulltermc  50619  postc  50677  islmd  50773  iscmd  50774