Theorem rexralbidv 1729

Description: Formula-building rule for restricted quantifiers (deduction rule).

Hypothesis

Ref	Expression
2ralbidv.1	⊢ (φ → (ψ ↔ χ))

Assertion

Ref	Expression
rexralbidv	⊢ (φ → (∃x ∈ A ∀y ∈ B ψ ↔ ∃x ∈ A ∀y ∈ B χ))

Distinct variable groups:   φ,x   φ,y

Proof of Theorem rexralbidv

Step	Hyp	Ref	Expression
1		2ralbidv.1	. . 3 ⊢ (φ → (ψ ↔ χ))
2	1	ralbidv 1710	. 2 ⊢ (φ → (∀y ∈ B ψ ↔ ∀y ∈ B χ))
3	2	rexbidv 1711	1 ⊢ (φ → (∃x ∈ A ∀y ∈ B ψ ↔ ∃x ∈ A ∀y ∈ B χ))

Syntax hints:   → wi 3   ↔ wb 153  ∀wral 1692  ∃wrex 1693

This theorem is referenced by:  freq1 2979  seq1bndi 7000  cvg2i 7012  caubndi 7016  clim 7067  clm4lei 7171  clmi1i 7176  climfnn 7182  2climnni 7192  2climnn0i 7193  climubii 7243  climcaui 7246  caucvglem1 7247  caucvgi 7253  caucvg3 7258  expcnvlem5 7321  elcncf 7355  ivthlem2 7372  ivthlem8 7378  lmfval 8010  caufval 8011  lmbr 8013  lmcvg 8017  iscau 8021  lmclim 8048  lmcau 8081  isgrp 8126  isring 8225  ringi 8226  ubthi 8628  hlimi 9139  hlim2 9143  hlimcauii 9189  hlimuniii 9191  occllem6 9261  riesz1 10081

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 1004  ax-17 1012  ax-4 1014  ax-5o 1016

This theorem depends on definitions:  df-bi 154  df-an 232  df-ex 1022  df-ral 1696  df-rex 1697

Copyright terms: Public domain