Theorem 2ralbidv 2554

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

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

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 1493  ax-gen 1495  ax-4 1556  ax-17 1572

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-ral 2513

This theorem is referenced by:  cbvral3v  2780  poeq1  4390  soeq1  4406  isoeq1  5925  isoeq2  5926  isoeq3  5927  fnmpoovd  6361  smoeq  6436  xpf1o  7005  tapeq1  7438  elinp  7661  cauappcvgpr  7849  seq3caopr2  10715  seqcaopr2g  10716  wrd2ind  11255  addcn2  11821  mulcn2  11823  sgrp1  13444  ismhm  13494  mhmex  13495  issubm  13505  isnsg  13739  nmznsg  13750  isghm  13780  iscmn  13830  ring1  14022  opprsubrngg  14175  issubrg3  14211  islmod  14255  lmodlema  14256  lsssetm  14320  islssmd  14323  islidlm  14443  ispsmet  14997  ismet  15018  isxmet  15019  addcncntoplem  15235  elcncf  15247  mpodvdsmulf1o  15664