Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > reximssdv | Structured version Visualization version GIF version |
Description: Derivation of a restricted existential quantification over a subset (the second hypothesis implies 𝐴 ⊆ 𝐵), deduction form. (Contributed by AV, 21-Aug-2022.) |
Ref | Expression |
---|---|
reximssdv.1 | ⊢ (𝜑 → ∃𝑥 ∈ 𝐵 𝜓) |
reximssdv.2 | ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝜓)) → 𝑥 ∈ 𝐴) |
reximssdv.3 | ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝜓)) → 𝜒) |
Ref | Expression |
---|---|
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 3230 | . 2 ⊢ (𝜑 → (∃𝑥 ∈ 𝐵 𝜓 → ∃𝑥 ∈ 𝐴 𝜒)) |
7 | 1, 6 | mpd 15 | 1 ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 𝜒) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 399 ∈ wcel 2111 ∃wrex 3107 |
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 1911 |
This theorem depends on definitions: df-bi 210 df-an 400 df-ex 1782 df-rex 3112 |
This theorem is referenced by: fin1a2lem6 9816 fpwwe2lem12 10052 pgpssslw 18731 efgrelexlemb 18868 lspsneq 19887 lbsextlem4 19926 neissex 21732 iscnp4 21868 nlly2i 22081 llynlly 22082 qtophmeo 22422 ovolicc2lem5 24125 itgsubst 24652 footexALT 26512 footex 26515 opphllem1 26541 lcfl6 38796 mapdval2N 38926 mapdpglem2 38969 hdmaprnlem10N 39155 pellfundglb 39826 |
Copyright terms: Public domain | W3C validator |