Theorem rexralbidv 2516

Description: Formula-building rule for restricted quantifiers (deduction form). (Contributed by NM, 28-Jan-2006.)

Hypothesis

Ref	Expression
2ralbidv.1	⊢ (𝜑 → (𝜓 ↔ 𝜒))

Assertion

Ref	Expression
rexralbidv	⊢ (𝜑 → (∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓 ↔ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜒))

Distinct variable groups:   𝜑,𝑥   𝜑,𝑦

Allowed substitution hints:   𝜓(𝑥,𝑦)   𝜒(𝑥,𝑦)   𝐴(𝑥,𝑦)   𝐵(𝑥,𝑦)

Proof of Theorem rexralbidv

Step	Hyp	Ref	Expression
1		2ralbidv.1	. . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
2	1	ralbidv 2490	. 2 ⊢ (𝜑 → (∀𝑦 ∈ 𝐵 𝜓 ↔ ∀𝑦 ∈ 𝐵 𝜒))
3	2	rexbidv 2491	1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓 ↔ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜒))

Syntax hints:   → wi 4   ↔ wb 105  ∀wral 2468  ∃wrex 2469

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 1458  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-4 1521  ax-17 1537  ax-ial 1545

This theorem depends on definitions:  df-bi 117  df-nf 1472  df-ral 2473  df-rex 2474

This theorem is referenced by:  caucvgpr  7716  caucvgprpr  7746  caucvgsrlemgt1  7829  caucvgsrlemoffres  7834  axcaucvglemres  7933  cvg1nlemres  11035  rexfiuz  11039  resqrexlemgt0  11070  resqrexlemoverl  11071  resqrexlemglsq  11072  resqrexlemsqa  11074  resqrexlemex  11075  cau3lem  11164  caubnd2  11167  climi  11336  2clim  11350  ennnfonelemim  12486  lmcvg  14202  lmss  14231  txlm  14264  metcnpi  14500  metcnpi2  14501  elcncf  14545  cncfi  14550  limcimo  14619  cnplimclemr  14623  limccoap  14632