![]() |
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 3164 | . 2 ⊢ (𝜑 → (∃𝑥 ∈ 𝐵 𝜓 → ∃𝑥 ∈ 𝐴 𝜒)) |
7 | 1, 6 | mpd 15 | 1 ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 𝜒) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 ∈ wcel 2106 ∃wrex 3070 |
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 1913 |
This theorem depends on definitions: df-bi 206 df-an 397 df-ex 1782 df-rex 3071 |
This theorem is referenced by: ttrcltr 9713 fin1a2lem6 10402 fpwwe2lem11 10638 pgpssslw 19484 efgrelexlemb 19620 lspsneq 20741 lbsextlem4 20780 neissex 22638 iscnp4 22774 nlly2i 22987 llynlly 22988 qtophmeo 23328 ovolicc2lem5 25045 itgsubst 25573 footexALT 28007 footex 28010 opphllem1 28036 irngnzply1 32815 lcfl6 40457 mapdval2N 40587 mapdpglem2 40630 hdmaprnlem10N 40816 pellfundglb 41705 oawordex2 42158 |
Copyright terms: Public domain | W3C validator |