Description: Derivation of a restricted existential quantification over a subset (the second hypothesis implies A C_ B ), deduction form. (Contributed by AV, 21-Aug-2022)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | reximssdv.1 | ⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝐵 𝜓 ) | |
| reximssdv.2 | ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝜓 ) ) → 𝑥 ∈ 𝐴 ) | ||
| reximssdv.3 | ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝜓 ) ) → 𝜒 ) | ||
| Assertion | reximssdv | ⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝐴 𝜒 ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | reximssdv.1 | ⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝐵 𝜓 ) | |
| 2 | reximssdv.2 | ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝜓 ) ) → 𝑥 ∈ 𝐴 ) | |
| 3 | reximssdv.3 | ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝜓 ) ) → 𝜒 ) | |
| 4 | 2 3 | jca | ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝜓 ) ) → ( 𝑥 ∈ 𝐴 ∧ 𝜒 ) ) |
| 5 | 4 | ex | ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐵 ∧ 𝜓 ) → ( 𝑥 ∈ 𝐴 ∧ 𝜒 ) ) ) |
| 6 | 5 | reximdv2 | ⊢ ( 𝜑 → ( ∃ 𝑥 ∈ 𝐵 𝜓 → ∃ 𝑥 ∈ 𝐴 𝜒 ) ) |
| 7 | 1 6 | mpd | ⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝐴 𝜒 ) |