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  4394  soeq1  4410  isoeq1  5937  isoeq2  5938  isoeq3  5939  fnmpoovd  6375  smoeq  6451  xpf1o  7025  tapeq1  7461  elinp  7684  cauappcvgpr  7872  seq3caopr2  10745  seqcaopr2g  10746  wrd2ind  11294  addcn2  11861  mulcn2  11863  sgrp1  13484  ismhm  13534  mhmex  13535  issubm  13545  isnsg  13779  nmznsg  13790  isghm  13820  iscmn  13870  ring1  14062  opprsubrngg  14215  issubrg3  14251  islmod  14295  lmodlema  14296  lsssetm  14360  islssmd  14363  islidlm  14483  ispsmet  15037  ismet  15058  isxmet  15059  addcncntoplem  15275  elcncf  15287  mpodvdsmulf1o  15704