| 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 511 | . . . 4 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝜓)) → (𝑥 ∈ 𝐴 ∧ 𝜒)) |
| 5 | 4 | ex 412 | . . 3 ⊢ (𝜑 → ((𝑥 ∈ 𝐵 ∧ 𝜓) → (𝑥 ∈ 𝐴 ∧ 𝜒))) |
| 6 | 5 | reximdv2 3164 | . 2 ⊢ (𝜑 → (∃𝑥 ∈ 𝐵 𝜓 → ∃𝑥 ∈ 𝐴 𝜒)) |
| 7 | 1, 6 | mpd 15 | 1 ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 𝜒) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∧ wa 395 ∈ wcel 2108 ∃wrex 3070 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1780 df-rex 3071 |
| This theorem is referenced by: ttrcltr 9756 fin1a2lem6 10445 fpwwe2lem11 10681 pgpssslw 19632 efgrelexlemb 19768 lspsneq 21124 lbsextlem4 21163 neissex 23135 iscnp4 23271 nlly2i 23484 llynlly 23485 qtophmeo 23825 ovolicc2lem5 25556 itgsubst 26090 footexALT 28726 footex 28729 opphllem1 28755 irngnzply1 33741 weiunfr 36468 lcfl6 41502 mapdval2N 41632 mapdpglem2 41675 hdmaprnlem10N 41861 primrootsunit1 42098 aks6d1c2 42131 aks6d1c6lem5 42178 aks5lem8 42202 pellfundglb 42896 oawordex2 43339 upciclem4 48926 |
| Copyright terms: Public domain | W3C validator |