Theorem reximssdv 3170

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

Step	Hyp	Ref	Expression
1		reximssdv.1	. 2 ⊢ (𝜑 → ∃𝑥 ∈ 𝐵 𝜓)
2		reximssdv.2	. . . . 5 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝜓)) → 𝑥 ∈ 𝐴)
3		reximssdv.3	. . . . 5 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝜓)) → 𝜒)
4	2, 3	jca 511	. . . 4 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝜓)) → (𝑥 ∈ 𝐴 ∧ 𝜒))
5	4	ex 412	. . 3 ⊢ (𝜑 → ((𝑥 ∈ 𝐵 ∧ 𝜓) → (𝑥 ∈ 𝐴 ∧ 𝜒)))
6	5	reximdv2 3161	. 2 ⊢ (𝜑 → (∃𝑥 ∈ 𝐵 𝜓 → ∃𝑥 ∈ 𝐴 𝜒))
7	1, 6	mpd 15	1 ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 𝜒)

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2105  ∃wrex 3067

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-rex 3068

This theorem is referenced by:  ttrcltr  9753  fin1a2lem6  10442  fpwwe2lem11  10678  pgpssslw  19646  efgrelexlemb  19782  lspsneq  21141  lbsextlem4  21180  neissex  23150  iscnp4  23286  nlly2i  23499  llynlly  23500  qtophmeo  23840  ovolicc2lem5  25569  itgsubst  26104  footexALT  28740  footex  28743  opphllem1  28769  irngnzply1  33705  weiunfr  36449  lcfl6  41482  mapdval2N  41612  mapdpglem2  41655  hdmaprnlem10N  41841  primrootsunit1  42078  aks6d1c2  42111  aks6d1c6lem5  42158  aks5lem8  42182  pellfundglb  42872  oawordex2  43315  upciclem4  48814