Theorem reximssdv 3183

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 520	. . . 4 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝜓)) → (𝑥 ∈ 𝐴 ∧ 𝜒))
5	4	ex 417	. . 3 ⊢ (𝜑 → ((𝑥 ∈ 𝐵 ∧ 𝜓) → (𝑥 ∈ 𝐴 ∧ 𝜒)))
6	5	reximdv2 3175	. 2 ⊢ (𝜑 → (∃𝑥 ∈ 𝐵 𝜓 → ∃𝑥 ∈ 𝐴 𝜒))
7	1, 6	mpd 16	1 ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 𝜒)

This proof depends on syntax axioms:   → wi 4   ∧ wa 400   ∈ wcel 2143  ∃wrex 3089

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940

This proof depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-rex 3090

This theorem is used by:  ttrcltr  9681  fin1a2lem6  10393  fpwwe2lem11  10630  pgpssslw  19688  efgrelexlemb  19824  lspsneq  21255  lbsextlem4  21294  neissex  23293  iscnp4  23429  nlly2i  23642  llynlly  23643  qtophmeo  23983  ovolicc2lem5  25689  itgsubst  26217  footexALT  29007  footex  29010  opphllem1  29037  irngnzply1  34090  weiunfr  37006  lcfl6  42302  mapdval2N  42432  mapdordlem2  42439  mapdpglem2  42475  hdmaprnlem10N  42661  primrootsunit1  42892  aks6d1c2  42925  aks6d1c6lem5  42972  aks5lem8  42996  pellfundglb  43640  oawordex2  44081  upciclem4  49975