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

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

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