Theorem 2ralbidv 2521

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

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

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 1461  ax-gen 1463  ax-4 1524  ax-17 1540

This theorem depends on definitions:  df-bi 117  df-nf 1475  df-ral 2480

This theorem is referenced by:  cbvral3v  2744  poeq1  4335  soeq1  4351  isoeq1  5851  isoeq2  5852  isoeq3  5853  fnmpoovd  6282  smoeq  6357  xpf1o  6914  tapeq1  7337  elinp  7560  cauappcvgpr  7748  seq3caopr2  10604  seqcaopr2g  10605  addcn2  11494  mulcn2  11496  sgrp1  13115  ismhm  13165  mhmex  13166  issubm  13176  isnsg  13410  nmznsg  13421  isghm  13451  iscmn  13501  ring1  13693  opprsubrngg  13845  issubrg3  13881  islmod  13925  lmodlema  13926  lsssetm  13990  islssmd  13993  islidlm  14113  ispsmet  14667  ismet  14688  isxmet  14689  addcncntoplem  14905  elcncf  14917  mpodvdsmulf1o  15334