Theorem 2ralbidv 2529

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

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

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 1469  ax-gen 1471  ax-4 1532  ax-17 1548

This theorem depends on definitions:  df-bi 117  df-nf 1483  df-ral 2488

This theorem is referenced by:  cbvral3v  2752  poeq1  4345  soeq1  4361  isoeq1  5869  isoeq2  5870  isoeq3  5871  fnmpoovd  6300  smoeq  6375  xpf1o  6940  tapeq1  7363  elinp  7586  cauappcvgpr  7774  seq3caopr2  10636  seqcaopr2g  10637  addcn2  11592  mulcn2  11594  sgrp1  13214  ismhm  13264  mhmex  13265  issubm  13275  isnsg  13509  nmznsg  13520  isghm  13550  iscmn  13600  ring1  13792  opprsubrngg  13944  issubrg3  13980  islmod  14024  lmodlema  14025  lsssetm  14089  islssmd  14092  islidlm  14212  ispsmet  14766  ismet  14787  isxmet  14788  addcncntoplem  15004  elcncf  15016  mpodvdsmulf1o  15433