| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > rexim | Structured version Visualization version GIF version | ||
| Description: Theorem 19.22 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 22-Nov-1994.) (Proof shortened by Andrew Salmon, 30-May-2011.) |
| Ref | Expression |
|---|---|
| rexim | ⊢ (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) → (∃𝑥 ∈ 𝐴 𝜑 → ∃𝑥 ∈ 𝐴 𝜓)) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | con3 153 | . . . 4 ⊢ ((𝜑 → 𝜓) → (¬ 𝜓 → ¬ 𝜑)) | |
| 2 | 1 | ral2imi 3085 | . . 3 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) → (∀𝑥 ∈ 𝐴 ¬ 𝜓 → ∀𝑥 ∈ 𝐴 ¬ 𝜑)) |
| 3 | ralnex 3072 | . . 3 ⊢ (∀𝑥 ∈ 𝐴 ¬ 𝜓 ↔ ¬ ∃𝑥 ∈ 𝐴 𝜓) | |
| 4 | ralnex 3072 | . . 3 ⊢ (∀𝑥 ∈ 𝐴 ¬ 𝜑 ↔ ¬ ∃𝑥 ∈ 𝐴 𝜑) | |
| 5 | 2, 3, 4 | 3imtr3g 295 | . 2 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) → (¬ ∃𝑥 ∈ 𝐴 𝜓 → ¬ ∃𝑥 ∈ 𝐴 𝜑)) |
| 6 | 5 | con4d 115 | 1 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) → (∃𝑥 ∈ 𝐴 𝜑 → ∃𝑥 ∈ 𝐴 𝜓)) |
| Colors of variables: wff setvar class |
| Syntax hints: ¬ wn 3 → wi 4 ∀wral 3061 ∃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 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1780 df-ral 3062 df-rex 3071 |
| This theorem is referenced by: reximiaOLD 3088 rexbi 3104 r19.35OLD 3109 r19.29OLD 3115 r19.30 3120 reximdvaiOLD 3166 reximdai 3261 reupick2 4331 ss2iun 5010 dfiun2g 5030 chfnrn 7069 isf32lem2 10394 psdmul 22170 ptcmplem4 24063 madebdayim 27926 madebdaylemold 27936 bnj110 34872 poimirlem25 37652 |
| Copyright terms: Public domain | W3C validator |