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

Theorem ssrexv 3232
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 3161 . . 3 (𝐴𝐵 → (𝑥𝐴𝑥𝐵))
21anim1d 336 . 2 (𝐴𝐵 → ((𝑥𝐴𝜑) → (𝑥𝐵𝜑)))
32reximdv2 2586 1 (𝐴𝐵 → (∃𝑥𝐴 𝜑 → ∃𝑥𝐵 𝜑))
Colors of variables: wff set class
Syntax hints:  wi 4  wcel 2158  wrex 2466  wss 3141
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 1457  ax-7 1458  ax-gen 1459  ax-ie1 1503  ax-ie2 1504  ax-8 1514  ax-11 1516  ax-4 1520  ax-17 1536  ax-i9 1540  ax-ial 1544  ax-i5r 1545  ax-ext 2169
This theorem depends on definitions:  df-bi 117  df-nf 1471  df-sb 1773  df-clab 2174  df-cleq 2180  df-clel 2183  df-rex 2471  df-in 3147  df-ss 3154
This theorem is referenced by:  iunss1  3909  moriotass  5872  tfr1onlemssrecs  6354  tfrcllemssrecs  6367  fiss  6990  supelti  7015  ctssdclemn0  7123  ctssdc  7126  enumctlemm  7127  nninfwlpoimlemginf  7188  rerecapb  8814  lbzbi  9630  fiubm  10822  rexico  11244  alzdvds  11874  zsupcl  11962  infssuzex  11964  gcddvds  11978  dvdslegcd  11979  pclemub  12301  subrgdvds  13455  ssrest  13978  reeff1olem  14488  bj-charfunbi  14859  bj-nn0suc  15012
  Copyright terms: Public domain W3C validator