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 512 | . . . 4 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝜓)) → (𝑥 ∈ 𝐴 ∧ 𝜒)) |
5 | 4 | ex 413 | . . 3 ⊢ (𝜑 → ((𝑥 ∈ 𝐵 ∧ 𝜓) → (𝑥 ∈ 𝐴 ∧ 𝜒))) |
6 | 5 | reximdv2 3268 | . 2 ⊢ (𝜑 → (∃𝑥 ∈ 𝐵 𝜓 → ∃𝑥 ∈ 𝐴 𝜒)) |
7 | 1, 6 | mpd 15 | 1 ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 𝜒) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 ∈ wcel 2105 ∃wrex 3136 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 |
This theorem depends on definitions: df-bi 208 df-an 397 df-ex 1772 df-rex 3141 |
This theorem is referenced by: fin1a2lem6 9815 fpwwe2lem12 10051 pgpssslw 18668 efgrelexlemb 18805 lspsneq 19823 lbsextlem4 19862 neissex 21663 iscnp4 21799 nlly2i 22012 llynlly 22013 qtophmeo 22353 ovolicc2lem5 24049 itgsubst 24573 footexALT 26431 footex 26434 opphllem1 26460 lcfl6 38516 mapdval2N 38646 mapdpglem2 38689 hdmaprnlem10N 38875 pellfundglb 39360 |
Copyright terms: Public domain | W3C validator |