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

Theorem reximssdv 3185
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 515 . . . 4 ((𝜑 ∧ (𝑥𝐵𝜓)) → (𝑥𝐴𝜒))
54ex 416 . . 3 (𝜑 → ((𝑥𝐵𝜓) → (𝑥𝐴𝜒)))
65reximdv2 3180 . 2 (𝜑 → (∃𝑥𝐵 𝜓 → ∃𝑥𝐴 𝜒))
71, 6mpd 15 1 (𝜑 → ∃𝑥𝐴 𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399  wcel 2113  wrex 3054
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1916
This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1787  df-rex 3059
This theorem is referenced by:  fin1a2lem6  9898  fpwwe2lem11  10134  pgpssslw  18850  efgrelexlemb  18987  lspsneq  20006  lbsextlem4  20045  neissex  21871  iscnp4  22007  nlly2i  22220  llynlly  22221  qtophmeo  22561  ovolicc2lem5  24266  itgsubst  24793  footexALT  26656  footex  26659  opphllem1  26685  lcfl6  39126  mapdval2N  39256  mapdpglem2  39299  hdmaprnlem10N  39485  pellfundglb  40263
  Copyright terms: Public domain W3C validator