Theorem 2ralbidva 3206

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 394   ∈ wcel 2098  ∀wral 3050

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905

This theorem depends on definitions:  df-bi 206  df-an 395  df-ral 3051

This theorem is referenced by:  disjxun  5147  reu3op  6298  opreu2reurex  6300  isocnv3  7339  isotr  7343  f1oweALT  7977  fnmpoovd  8092  pospropd  18322  tosso  18414  isipodrs  18532  mgmpropd  18614  mgmhmpropd  18661  sgrppropd  18694  mndpropd  18722  mhmpropd  18752  efgred  19715  cmnpropd  19758  rngpropd  20126  ringpropd  20236  lmodprop2d  20819  lsspropd  20914  islmhm2  20935  lmhmpropd  20970  isdomn3  21265  islindf4  21789  assapropd  21822  scmatmats  22457  cpmatel2  22659  1elcpmat  22661  m2cpminvid2  22701  decpmataa0  22714  pmatcollpw2lem  22723  connsub  23369  hausdiag  23593  ist0-4  23677  ismet2  24283  txmetcnp  24500  txmetcn  24501  metuel2  24518  metucn  24524  isngp3  24551  nlmvscn  24648  isclmp  25068  isncvsngp  25121  ipcn  25218  iscfil2  25238  caucfil  25255  cfilresi  25267  ulmdvlem3  26383  cxpcn3  26728  tgjustf  28349  tgjustr  28350  tgcgr4  28407  perpcom  28589  brbtwn2  28788  colinearalglem2  28790  eengtrkg  28869  isarchi2  32985  opprlidlabs  33297  elmrsubrn  35261  isbnd3b  37389  iscvlat2N  38926  ishlat3N  38956  gicabl  42665  lindslinindsimp2  47717  joindm3  48174  meetdm3  48176  functhinclem1  48233  postc  48274