Theorem 2ralbidv 2556

Description: Formula-building rule for restricted universal quantifiers (deduction form). (Contributed by NM, 28-Jan-2006.) (Revised by Szymon Jaroszewicz, 16-Mar-2007.)

Hypothesis

Ref	Expression
2ralbidv.1	⊢ (𝜑 → (𝜓 ↔ 𝜒))

Assertion

Ref	Expression
2ralbidv	⊢ (𝜑 → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜒))

Distinct variable groups:   𝜑,𝑥   𝜑,𝑦

Allowed substitution hints:   𝜓(𝑥,𝑦)   𝜒(𝑥,𝑦)   𝐴(𝑥,𝑦)   𝐵(𝑥,𝑦)

Proof of Theorem 2ralbidv

Step	Hyp	Ref	Expression
1		2ralbidv.1	. . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
2	1	ralbidv 2532	. 2 ⊢ (𝜑 → (∀𝑦 ∈ 𝐵 𝜓 ↔ ∀𝑦 ∈ 𝐵 𝜒))
3	2	ralbidv 2532	1 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜒))

Syntax hints:   → wi 4   ↔ wb 105  ∀wral 2510

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1495  ax-gen 1497  ax-4 1558  ax-17 1574

This theorem depends on definitions:  df-bi 117  df-nf 1509  df-ral 2515

This theorem is referenced by:  cbvral3v  2782  poeq1  4396  soeq1  4412  isoeq1  5942  isoeq2  5943  isoeq3  5944  fnmpoovd  6380  smoeq  6456  xpf1o  7030  tapeq1  7471  elinp  7694  cauappcvgpr  7882  seq3caopr2  10756  seqcaopr2g  10757  wrd2ind  11308  addcn2  11888  mulcn2  11890  sgrp1  13512  ismhm  13562  mhmex  13563  issubm  13573  isnsg  13807  nmznsg  13818  isghm  13848  iscmn  13898  ring1  14091  opprsubrngg  14244  issubrg3  14280  islmod  14324  lmodlema  14325  lsssetm  14389  islssmd  14392  islidlm  14512  ispsmet  15066  ismet  15087  isxmet  15088  addcncntoplem  15304  elcncf  15316  mpodvdsmulf1o  15733