Theorem 2ralbidva 3229

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

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

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 3082

This theorem is used by:  disjxun  5109  reu3op  6298  opreu2reurex  6300  isocnv3  7340  isotr  7344  f1oweALT  7976  fnmpoovd  8089  pospropd  18408  tosso  18500  isipodrs  18620  mgmpropd  18738  mgmhmpropd  18793  sgrppropd  18826  mndpropd  18857  mhmpropd  18892  efgred  19867  cmnpropd  19910  rngpropd  20301  ringpropd  20422  isdomn3  20868  lmodprop2d  21100  lsspropd  21193  islmhm2  21214  lmhmpropd  21249  df2idl2crng  21476  islindf4  22043  assapropd  22076  scmatmats  22723  cpmatel2  22925  1elcpmat  22927  m2cpminvid2  22967  decpmataa0  22980  pmatcollpw2lem  22989  connsub  23633  hausdiag  23858  ist0-4  23942  ismet2  24546  txmetcnp  24760  txmetcn  24761  metuel2  24778  metucn  24784  isngp3  24811  nlmvscn  24900  isclmp  25312  isncvsngp  25364  ipcn  25461  iscfil2  25481  caucfil  25498  cfilresi  25510  ulmdvlem3  26621  cxpcn3  26969  tgjustf  28798  tgjustr  28799  tgcgr4  28856  perpcom  29049  brbtwn2  29315  colinearalglem2  29317  eengtrkg  29396  isarchi2  33574  opprlidlabs  33836  elmrsubrn  36054  nmulprop  36724  nmulcom  36728  nadddilem2  36755  nadddilem4  36757  isbnd3b  38499  iscvlat2N  40161  ishlat3N  40191  gicabl  43904  lindslinindsimp2  49320  joindm3  49824  meetdm3  49826  fucofulem2  50166  thincpropd  50297  functhinclem1  50299  fulltermc  50366  postc  50424  islmd  50520  iscmd  50521