Theorem 2ralbidv 2530

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

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

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 1470  ax-gen 1472  ax-4 1533  ax-17 1549

This theorem depends on definitions:  df-bi 117  df-nf 1484  df-ral 2489

This theorem is referenced by:  cbvral3v  2753  poeq1  4346  soeq1  4362  isoeq1  5870  isoeq2  5871  isoeq3  5872  fnmpoovd  6301  smoeq  6376  xpf1o  6941  tapeq1  7364  elinp  7587  cauappcvgpr  7775  seq3caopr2  10638  seqcaopr2g  10639  addcn2  11621  mulcn2  11623  sgrp1  13243  ismhm  13293  mhmex  13294  issubm  13304  isnsg  13538  nmznsg  13549  isghm  13579  iscmn  13629  ring1  13821  opprsubrngg  13973  issubrg3  14009  islmod  14053  lmodlema  14054  lsssetm  14118  islssmd  14121  islidlm  14241  ispsmet  14795  ismet  14816  isxmet  14817  addcncntoplem  15033  elcncf  15045  mpodvdsmulf1o  15462