MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  reximssdv Structured version   Visualization version   GIF version

Theorem reximssdv 3199
Description: Derivation of a restricted existential quantification over a subset (the second hypothesis implies 𝐴𝐵), deduction form. (Contributed by AV, 21-Aug-2022.)
Hypotheses
Ref Expression
reximssdv.1 (𝜑 → ∃𝑥𝐵 𝜓)
reximssdv.2 ((𝜑 ∧ (𝑥𝐵𝜓)) → 𝑥𝐴)
reximssdv.3 ((𝜑 ∧ (𝑥𝐵𝜓)) → 𝜒)
Assertion
Ref Expression
reximssdv (𝜑 → ∃𝑥𝐴 𝜒)
Distinct variable group:   𝜑,𝑥
Allowed substitution hints:   𝜓(𝑥)   𝜒(𝑥)   𝐴(𝑥)   𝐵(𝑥)

Proof of Theorem reximssdv
StepHypRef Expression
1 reximssdv.1 . 2 (𝜑 → ∃𝑥𝐵 𝜓)
2 reximssdv.2 . . . . 5 ((𝜑 ∧ (𝑥𝐵𝜓)) → 𝑥𝐴)
3 reximssdv.3 . . . . 5 ((𝜑 ∧ (𝑥𝐵𝜓)) → 𝜒)
42, 3jca 508 . . . 4 ((𝜑 ∧ (𝑥𝐵𝜓)) → (𝑥𝐴𝜒))
54ex 402 . . 3 (𝜑 → ((𝑥𝐵𝜓) → (𝑥𝐴𝜒)))
65reximdv2 3194 . 2 (𝜑 → (∃𝑥𝐵 𝜓 → ∃𝑥𝐴 𝜒))
71, 6mpd 15 1 (𝜑 → ∃𝑥𝐴 𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 385  wcel 2157  wrex 3090
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006
This theorem depends on definitions:  df-bi 199  df-an 386  df-ex 1876  df-rex 3095
This theorem is referenced by:  fin1a2lem6  9515  fpwwe2lem12  9751  pgpssslw  18342  efgrelexlemb  18478  lspsneq  19443  lbsextlem4  19484  neissex  21260  iscnp4  21396  nlly2i  21608  llynlly  21609  qtophmeo  21949  ovolicc2lem5  23629  itgsubst  24153  opphllem1  25995  lcfl6  37521  mapdval2N  37651  mapdpglem2  37694  hdmaprnlem10N  37880  pellfundglb  38235
  Copyright terms: Public domain W3C validator