Theorem ssrexv 3235

Description: Existential quantification restricted to a subclass. (Contributed by NM, 11-Jan-2007.)

Assertion

Ref	Expression
ssrexv	|- ( A C_ B -> ( E. x e. A ph -> E. x e. B ph ) )

Distinct variable groups:   x, A   x, B

Allowed substitution hint:   ph( x)

Proof of Theorem ssrexv

Step	Hyp	Ref	Expression
1		ssel 3164	. . 3 |- ( A C_ B -> ( x e. A -> x e. B ) )
2	1	anim1d 336	. 2 |- ( A C_ B -> ( ( x e. A /\ ph ) -> ( x e. B /\ ph ) ) )
3	2	reximdv2 2589	1 |- ( A C_ B -> ( E. x e. A ph -> E. x e. B ph ) )

Syntax hints:   -> wi 4   e. wcel 2160   E.wrex 2469   C_ wss 3144

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-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-11 1517  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2171

This theorem depends on definitions:  df-bi 117  df-nf 1472  df-sb 1774  df-clab 2176  df-cleq 2182  df-clel 2185  df-rex 2474  df-in 3150  df-ss 3157

This theorem is referenced by:  iunss1  3912  moriotass  5880  tfr1onlemssrecs  6364  tfrcllemssrecs  6377  fiss  7006  supelti  7031  ctssdclemn0  7139  ctssdc  7142  enumctlemm  7143  nninfwlpoimlemginf  7204  rerecapb  8830  lbzbi  9646  fiubm  10840  rexico  11262  alzdvds  11892  zsupcl  11980  infssuzex  11982  gcddvds  11996  dvdslegcd  11997  pclemub  12319  subrgdvds  13582  ssrest  14139  reeff1olem  14649  bj-charfunbi  15021  bj-nn0suc  15174