Theorem 2ralbidv 2557

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

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

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 1496  ax-gen 1498  ax-4 1559  ax-17 1575

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-ral 2516

This theorem is referenced by:  cbvral3v  2783  poeq1  4402  soeq1  4418  isoeq1  5952  isoeq2  5953  isoeq3  5954  fnmpoovd  6389  smoeq  6499  xpf1o  7073  tapeq1  7531  elinp  7754  cauappcvgpr  7942  seq3caopr2  10818  seqcaopr2g  10819  wrd2ind  11370  addcn2  11950  mulcn2  11952  sgrp1  13574  ismhm  13624  mhmex  13625  issubm  13635  isnsg  13869  nmznsg  13880  isghm  13910  iscmn  13960  ring1  14153  opprsubrngg  14306  issubrg3  14342  islmod  14387  lmodlema  14388  lsssetm  14452  islssmd  14455  islidlm  14575  ispsmet  15134  ismet  15155  isxmet  15156  addcncntoplem  15372  elcncf  15384  mpodvdsmulf1o  15804