Theorem 2ralbidva 3199

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∈ wcel 2109  ∀wral 3044

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910

This theorem depends on definitions:  df-bi 207  df-an 396  df-ral 3045

This theorem is referenced by:  disjxun  5105  reu3op  6265  opreu2reurex  6267  isocnv3  7307  isotr  7311  f1oweALT  7951  fnmpoovd  8066  pospropd  18286  tosso  18378  isipodrs  18496  mgmpropd  18578  mgmhmpropd  18625  sgrppropd  18658  mndpropd  18686  mhmpropd  18719  efgred  19678  cmnpropd  19721  rngpropd  20083  ringpropd  20197  isdomn3  20624  lmodprop2d  20830  lsspropd  20924  islmhm2  20945  lmhmpropd  20980  islindf4  21747  assapropd  21781  scmatmats  22398  cpmatel2  22600  1elcpmat  22602  m2cpminvid2  22642  decpmataa0  22655  pmatcollpw2lem  22664  connsub  23308  hausdiag  23532  ist0-4  23616  ismet2  24221  txmetcnp  24435  txmetcn  24436  metuel2  24453  metucn  24459  isngp3  24486  nlmvscn  24575  isclmp  24997  isncvsngp  25049  ipcn  25146  iscfil2  25166  caucfil  25183  cfilresi  25195  ulmdvlem3  26311  cxpcn3  26658  tgjustf  28400  tgjustr  28401  tgcgr4  28458  perpcom  28640  brbtwn2  28832  colinearalglem2  28834  eengtrkg  28913  isarchi2  33139  opprlidlabs  33456  elmrsubrn  35507  isbnd3b  37779  iscvlat2N  39317  ishlat3N  39347  gicabl  43088  lindslinindsimp2  48452  joindm3  48957  meetdm3  48959  fucofulem2  49300  thincpropd  49431  functhinclem1  49433  fulltermc  49500  postc  49558  islmd  49654  iscmd  49655