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

Theorem ssrexv 3220
Description: Existential quantification restricted to a subclass. (Contributed by NM, 11-Jan-2007.)
Assertion
Ref Expression
ssrexv (𝐴𝐵 → (∃𝑥𝐴 𝜑 → ∃𝑥𝐵 𝜑))
Distinct variable groups:   𝑥,𝐴   𝑥,𝐵
Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem ssrexv
StepHypRef Expression
1 ssel 3149 . . 3 (𝐴𝐵 → (𝑥𝐴𝑥𝐵))
21anim1d 336 . 2 (𝐴𝐵 → ((𝑥𝐴𝜑) → (𝑥𝐵𝜑)))
32reximdv2 2576 1 (𝐴𝐵 → (∃𝑥𝐴 𝜑 → ∃𝑥𝐵 𝜑))
Colors of variables: wff set class
Syntax hints:  wi 4  wcel 2148  wrex 2456  wss 3129
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 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-11 1506  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159
This theorem depends on definitions:  df-bi 117  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-rex 2461  df-in 3135  df-ss 3142
This theorem is referenced by:  iunss1  3897  moriotass  5858  tfr1onlemssrecs  6339  tfrcllemssrecs  6352  fiss  6975  supelti  7000  ctssdclemn0  7108  ctssdc  7111  enumctlemm  7112  nninfwlpoimlemginf  7173  rerecapb  8799  lbzbi  9615  fiubm  10807  rexico  11229  alzdvds  11859  zsupcl  11947  infssuzex  11949  gcddvds  11963  dvdslegcd  11964  pclemub  12286  subrgdvds  13354  ssrest  13652  reeff1olem  14162  bj-charfunbi  14533  bj-nn0suc  14686
  Copyright terms: Public domain W3C validator