Theorem ssrexv 3266

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

Syntax hints:   -> wi 4   e. wcel 2178   E.wrex 2487   C_ wss 3174

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 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-11 1530  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2189

This theorem depends on definitions:  df-bi 117  df-nf 1485  df-sb 1787  df-clab 2194  df-cleq 2200  df-clel 2203  df-rex 2492  df-in 3180  df-ss 3187

This theorem is referenced by:  iunss1  3952  moriotass  5951  tfr1onlemssrecs  6448  tfrcllemssrecs  6461  fiss  7105  supelti  7130  ctssdclemn0  7238  ctssdc  7241  enumctlemm  7242  nninfwlpoimlemginf  7304  ficardon  7322  rerecapb  8951  lbzbi  9772  zsupcl  10411  infssuzex  10413  fiubm  11010  rexico  11647  alzdvds  12280  bitsfzolem  12380  gcddvds  12399  dvdslegcd  12400  pclemub  12725  subrgdvds  14112  ssrest  14769  plyss  15325  reeff1olem  15358  bj-charfunbi  15946  bj-nn0suc  16099