Theorem reubidva 3125

Description: Formula-building rule for restricted existential quantifier (deduction rule). (Contributed by NM, 13-Nov-2004.)

Hypothesis

Ref	Expression
reubidva.1	|- ( ( ph /\ x e. A ) -> ( ps <-> ch ) )

Assertion

Ref	Expression
reubidva	|- ( ph -> ( E! x e. A ps <-> E! x e. A ch ) )

Distinct variable group:   ph, x

Allowed substitution hints:   ps( x)   ch( x)   A( x)

Proof of Theorem reubidva

Step	Hyp	Ref	Expression
1		nfv 1843	. 2 |- F/ x ph
2		reubidva.1	. 2 |- ( ( ph /\ x e. A ) -> ( ps <-> ch ) )
3	1, 2	reubida 3124	1 |- ( ph -> ( E! x e. A ps <-> E! x e. A ch ) )

Syntax hints:   -> wi 4   <-> wb 196   /\ wa 384   e. wcel 1990   E!wreu 2914

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-12 2047

This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1705  df-nf 1710  df-eu 2474  df-reu 2919

This theorem is referenced by:  reubidv  3126  reuxfr2d  4891  reuxfrd  4893  exfo  6377  f1ofveu  6645  zmax  11785  zbtwnre  11786  rebtwnz  11787  icoshftf1o  12295  divalgb  15127  1arith2  15632  ply1divalg2  23898  frgr2wwlkeu  27191  numclwwlk2lem1  27235  numclwlk2lem2f1o  27238  pjhtheu2  28275  reuxfr3d  29329  reuxfr4d  29330  xrsclat  29680  xrmulc1cn  29976  poimirlem25  33434  hdmap14lem14  37173