![]() |
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 513 | . . . 4 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝜓)) → (𝑥 ∈ 𝐴 ∧ 𝜒)) |
5 | 4 | ex 414 | . . 3 ⊢ (𝜑 → ((𝑥 ∈ 𝐵 ∧ 𝜓) → (𝑥 ∈ 𝐴 ∧ 𝜒))) |
6 | 5 | reximdv2 3165 | . 2 ⊢ (𝜑 → (∃𝑥 ∈ 𝐵 𝜓 → ∃𝑥 ∈ 𝐴 𝜒)) |
7 | 1, 6 | mpd 15 | 1 ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 𝜒) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 397 ∈ wcel 2107 ∃wrex 3071 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 |
This theorem depends on definitions: df-bi 206 df-an 398 df-ex 1783 df-rex 3072 |
This theorem is referenced by: ttrcltr 9711 fin1a2lem6 10400 fpwwe2lem11 10636 pgpssslw 19482 efgrelexlemb 19618 lspsneq 20735 lbsextlem4 20774 neissex 22631 iscnp4 22767 nlly2i 22980 llynlly 22981 qtophmeo 23321 ovolicc2lem5 25038 itgsubst 25566 footexALT 27969 footex 27972 opphllem1 27998 irngnzply1 32755 lcfl6 40371 mapdval2N 40501 mapdpglem2 40544 hdmaprnlem10N 40730 pellfundglb 41623 oawordex2 42076 |
Copyright terms: Public domain | W3C validator |