Theorem ssrexv 3290

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 3219	. . 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 2629	1 |- ( A C_ B -> ( E. x e. A ph -> E. x e. B ph ) )

Syntax hints:   -> wi 4   e. wcel 2200   E.wrex 2509   C_ wss 3198

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 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-11 1552  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-rex 2514  df-in 3204  df-ss 3211

This theorem is referenced by:  iunss1  3979  moriotass  5997  tfr1onlemssrecs  6500  tfrcllemssrecs  6513  fiss  7167  supelti  7192  ctssdclemn0  7300  ctssdc  7303  enumctlemm  7304  nninfwlpoimlemginf  7366  ficardon  7384  rerecapb  9013  lbzbi  9840  zsupcl  10481  infssuzex  10483  fiubm  11082  rexico  11772  alzdvds  12405  bitsfzolem  12505  gcddvds  12524  dvdslegcd  12525  pclemub  12850  subrgdvds  14239  ssrest  14896  plyss  15452  reeff1olem  15485  bj-charfunbi  16342  bj-nn0suc  16495