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

Theorem reximssdv 3172
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 512 . . . 4 ((𝜑 ∧ (𝑥𝐵𝜓)) → (𝑥𝐴𝜒))
54ex 413 . . 3 (𝜑 → ((𝑥𝐵𝜓) → (𝑥𝐴𝜒)))
65reximdv2 3164 . 2 (𝜑 → (∃𝑥𝐵 𝜓 → ∃𝑥𝐴 𝜒))
71, 6mpd 15 1 (𝜑 → ∃𝑥𝐴 𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  wcel 2106  wrex 3070
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913
This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-rex 3071
This theorem is referenced by:  ttrcltr  9713  fin1a2lem6  10402  fpwwe2lem11  10638  pgpssslw  19484  efgrelexlemb  19620  lspsneq  20741  lbsextlem4  20780  neissex  22638  iscnp4  22774  nlly2i  22987  llynlly  22988  qtophmeo  23328  ovolicc2lem5  25045  itgsubst  25573  footexALT  28007  footex  28010  opphllem1  28036  irngnzply1  32815  lcfl6  40457  mapdval2N  40587  mapdpglem2  40630  hdmaprnlem10N  40816  pellfundglb  41705  oawordex2  42158
  Copyright terms: Public domain W3C validator