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 3082 | . . 3 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) → (∀𝑥 ∈ 𝐴 ¬ 𝜓 → ∀𝑥 ∈ 𝐴 ¬ 𝜑)) |
3 | ralnex 3167 | . . 3 ⊢ (∀𝑥 ∈ 𝐴 ¬ 𝜓 ↔ ¬ ∃𝑥 ∈ 𝐴 𝜓) | |
4 | ralnex 3167 | . . 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 3064 ∃wrex 3065 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 |
This theorem depends on definitions: df-bi 206 df-an 397 df-ex 1783 df-ral 3069 df-rex 3070 |
This theorem is referenced by: rexbi 3173 reximiaOLD 3177 r19.29 3184 reximdvaiOLD 3201 reximdai 3244 r19.30 3268 r19.35 3271 reupick2 4254 ss2iun 4942 dfiun2g 4960 chfnrn 6926 isf32lem2 10110 ptcmplem4 23206 bnj110 32838 madebdayim 34070 madebdaylemold 34078 poimirlem25 35802 |
Copyright terms: Public domain | W3C validator |