Theorem reximssdv 3151

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 3143	. 2 ⊢ (𝜑 → (∃𝑥 ∈ 𝐵 𝜓 → ∃𝑥 ∈ 𝐴 𝜒))
7	1, 6	mpd 15	1 ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 𝜒)

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2109  ∃wrex 3053

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-rex 3054

This theorem is referenced by:  ttrcltr  9645  fin1a2lem6  10334  fpwwe2lem11  10570  pgpssslw  19528  efgrelexlemb  19664  lspsneq  21064  lbsextlem4  21103  neissex  23047  iscnp4  23183  nlly2i  23396  llynlly  23397  qtophmeo  23737  ovolicc2lem5  25455  itgsubst  25989  footexALT  28698  footex  28701  opphllem1  28727  irngnzply1  33679  weiunfr  36448  lcfl6  41487  mapdval2N  41617  mapdpglem2  41660  hdmaprnlem10N  41846  primrootsunit1  42078  aks6d1c2  42111  aks6d1c6lem5  42158  aks5lem8  42182  pellfundglb  42866  oawordex2  43308  upciclem4  49151