Theorem rexralbidv 1682

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

Hypothesis

Ref	Expression
2ralbidv.1	|- (ph -> (ps <-> ch))

Assertion

Ref	Expression
rexralbidv	|- (ph -> (E.x e. A A.y e. B ps <-> E.x e. A A.y e. B ch))

Distinct variable groups:   ph,x   ph,y

Proof of Theorem rexralbidv

Step	Hyp	Ref	Expression
1		2ralbidv.1	. . 3 |- (ph -> (ps <-> ch))
2	1	ralbidv 1663	. 2 |- (ph -> (A.y e. B ps <-> A.y e. B ch))
3	2	rexbidv 1664	1 |- (ph -> (E.x e. A A.y e. B ps <-> E.x e. A A.y e. B ch))

Syntax hints:   -> wi 3   <-> wb 146  A.wral 1645  E.wrex 1646

This theorem is referenced by:  freq1 2922  seq1bnd 6910  cvg2 6922  caubnd 6926  clim 6977  clm4le 7081  clmi1 7086  climfnn 7092  2climnn 7102  2climnn0 7103  climubi 7153  climcau 7156  caucvglem1 7157  caucvg 7163  caucvg3t 7168  expcnvlem5 7231  elcncf 7265  ivthlem2 7282  ivthlem8 7288  lmfval 7925  caufval 7926  lmbr 7928  lmcvg 7932  iscau 7936  lmclim 7963  lmcau 7996  isgrp 8041  isring 8141  ringi 8142  ubthi 8544  hlim 9056  hlim2 9060  hlimcaui 9106  hlimunii 9108  occllem6 9178  riesz1t 9998

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 963  ax-17 971  ax-4 973  ax-5o 975

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 981  df-ral 1649  df-rex 1650

Copyright terms: Public domain