MPE Home 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