Theorem ssrexv 3292

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

Syntax hints:   -> wi 4   e. wcel 2202   E.wrex 2511   C_ wss 3200

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 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-11 1554  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-rex 2516  df-in 3206  df-ss 3213

This theorem is referenced by:  iunss1  3981  moriotass  6001  tfr1onlemssrecs  6504  tfrcllemssrecs  6517  fiss  7175  supelti  7200  ctssdclemn0  7308  ctssdc  7311  enumctlemm  7312  nninfwlpoimlemginf  7374  ficardon  7392  rerecapb  9022  lbzbi  9849  zsupcl  10490  infssuzex  10492  fiubm  11091  rexico  11781  alzdvds  12414  bitsfzolem  12514  gcddvds  12533  dvdslegcd  12534  pclemub  12859  subrgdvds  14248  ssrest  14905  plyss  15461  reeff1olem  15494  bj-charfunbi  16406  bj-nn0suc  16559