Theorem 2ralbidv 2566

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

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

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 2525

This theorem is referenced by:  cbvral3v  2793  poeq1  4420  soeq1  4436  isoeq1  5974  isoeq2  5975  isoeq3  5976  fnmpoovd  6411  smoeq  6521  xpf1o  7097  papcotr  7562  tapeq1  7566  elinp  7789  cauappcvgpr  7977  seq3caopr2  10855  seqcaopr2g  10856  wrd2ind  11415  addcn2  11995  mulcn2  11997  sgrp1  13624  ismhm  13674  mhmex  13675  issubm  13685  isnsg  13919  nmznsg  13930  isghm  13960  iscmn  14010  ring1  14203  opprsubrngg  14356  issubrg3  14392  islmod  14439  lmodlema  14440  lsssetm  14504  islssmd  14507  islidlm  14627  ispsmet  15188  ismet  15209  isxmet  15210  addcncntoplem  15426  elcncf  15438  mpodvdsmulf1o  15858