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  11305  addcn2  11872  mulcn2  11874  sgrp1  13496  ismhm  13546  mhmex  13547  issubm  13557  isnsg  13791  nmznsg  13802  isghm  13832  iscmn  13882  ring1  14075  opprsubrngg  14228  issubrg3  14264  islmod  14308  lmodlema  14309  lsssetm  14373  islssmd  14376  islidlm  14496  ispsmet  15050  ismet  15071  isxmet  15072  addcncntoplem  15288  elcncf  15300  mpodvdsmulf1o  15717