Theorem 2ralbidv 2574

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

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

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 1500  ax-gen 1502  ax-4 1563  ax-17 1579

This theorem depends on definitions:  df-bi 117  df-nf 1514  df-ral 2533

This theorem is referenced by:  cbvral3v  2801  poeq1  4439  soeq1  4455  isoeq1  5997  isoeq2  5998  isoeq3  5999  fnmpoovd  6441  smoeq  6551  xpf1o  7134  papeq1  7599  papcotr  7603  tapeq1  7608  elinp  7831  cauappcvgpr  8019  seq3caopr2  10908  seqcaopr2g  10909  wrd2ind  11473  addcn2  12054  mulcn2  12056  sgrp1  13703  ismhm  13745  mhmex  13746  issubm  13756  isnsg  13982  nmznsg  13993  isghm  14023  iscmn  14073  ring1  14337  opprsubrngg  14492  issubrg3  14528  islmod  14600  lmodlema  14601  lsssetm  14665  islssmd  14668  islidlm  14788  ispsmet  15347  ismet  15368  isxmet  15369  addcncntoplem  15585  elcncf  15597  mpodvdsmulf1o  16018