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

Theorem reximssdv 3276
 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 514 . . . 4 ((𝜑 ∧ (𝑥𝐵𝜓)) → (𝑥𝐴𝜒))
54ex 415 . . 3 (𝜑 → ((𝑥𝐵𝜓) → (𝑥𝐴𝜒)))
65reximdv2 3271 . 2 (𝜑 → (∃𝑥𝐵 𝜓 → ∃𝑥𝐴 𝜒))
71, 6mpd 15 1 (𝜑 → ∃𝑥𝐴 𝜒)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 398   ∈ wcel 2110  ∃wrex 3139 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907 This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1777  df-rex 3144 This theorem is referenced by:  fin1a2lem6  9826  fpwwe2lem12  10062  pgpssslw  18738  efgrelexlemb  18875  lspsneq  19893  lbsextlem4  19932  neissex  21734  iscnp4  21870  nlly2i  22083  llynlly  22084  qtophmeo  22424  ovolicc2lem5  24121  itgsubst  24645  footexALT  26503  footex  26506  opphllem1  26532  lcfl6  38635  mapdval2N  38765  mapdpglem2  38808  hdmaprnlem10N  38994  pellfundglb  39480
 Copyright terms: Public domain W3C validator