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 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜒))

This proof depends on syntax axioms:   → wi 4   ↔ wb 105  ∀wral 2528

This proof depends on 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 proof depends on definitions:  df-bi 117  df-nf 1514  df-ral 2533

This theorem is used by:  cbvral3v  2801  poeq1  4444  soeq1  4460  isoeq1  6007  isoeq2  6008  isoeq3  6009  fnmpoovd  6451  smoeq  6561  xpf1o  7144  papeq1  7609  papcotr  7613  tapeq1  7618  elinp  7841  cauappcvgpr  8029  seq3caopr2  10930  seqcaopr2g  10931  wrd2ind  11495  addcn2  12076  mulcn2  12078  sgrp1  13726  ismhm  13768  mhmex  13769  issubm  13779  isnsg  14005  nmznsg  14016  isghm  14046  iscmn  14096  ring1  14364  opprsubrngg  14519  issubrg3  14555  islmod  14627  lmodlema  14628  lsssetm  14693  islssmd  14696  islidlm  14816  ispsmet  15424  ismet  15445  isxmet  15446  addcncntoplem  15662  elcncf  15674  mpodvdsmulf1o  16104