ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  ssrexv Unicode version

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
StepHypRef Expression
1 ssel 3164 . . 3  |-  ( A 
C_  B  ->  (
x  e.  A  ->  x  e.  B )
)
21anim1d 336 . 2  |-  ( A 
C_  B  ->  (
( x  e.  A  /\  ph )  ->  (
x  e.  B  /\  ph ) ) )
32reximdv2 2589 1  |-  ( A 
C_  B  ->  ( E. x  e.  A  ph 
->  E. x  e.  B  ph ) )
Colors of variables: wff set class
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
  Copyright terms: Public domain W3C validator