Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > reximdai | Structured version Visualization version GIF version |
Description: Deduction from Theorem 19.22 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 31-Aug-1999.) |
Ref | Expression |
---|---|
reximdai.1 | ⊢ Ⅎ𝑥𝜑 |
reximdai.2 | ⊢ (𝜑 → (𝑥 ∈ 𝐴 → (𝜓 → 𝜒))) |
Ref | Expression |
---|---|
reximdai | ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → ∃𝑥 ∈ 𝐴 𝜒)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | reximdai.1 | . . 3 ⊢ Ⅎ𝑥𝜑 | |
2 | reximdai.2 | . . 3 ⊢ (𝜑 → (𝑥 ∈ 𝐴 → (𝜓 → 𝜒))) | |
3 | 1, 2 | ralrimi 2940 | . 2 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 (𝜓 → 𝜒)) |
4 | rexim 2991 | . 2 ⊢ (∀𝑥 ∈ 𝐴 (𝜓 → 𝜒) → (∃𝑥 ∈ 𝐴 𝜓 → ∃𝑥 ∈ 𝐴 𝜒)) | |
5 | 3, 4 | syl 17 | 1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → ∃𝑥 ∈ 𝐴 𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 Ⅎwnf 1699 ∈ wcel 1977 ∀wral 2896 ∃wrex 2897 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-12 2034 |
This theorem depends on definitions: df-bi 196 df-an 385 df-ex 1696 df-nf 1701 df-ral 2901 df-rex 2902 |
This theorem is referenced by: tz7.49 7427 hsmexlem2 9132 acunirnmpt2 28842 acunirnmpt2f 28843 locfinreflem 29235 cmpcref 29245 indexdom 32699 filbcmb 32705 cdlemefr29exN 34708 rexanuz3 38303 disjrnmpt2 38370 fompt 38374 disjinfi 38375 iunmapsn 38404 supxrge 38495 suplesup 38496 infxr 38524 allbutfi 38557 limsupre 38708 stoweidlem31 38924 stoweidlem34 38927 fourierdlem73 39072 sge0pnffigt 39289 sge0ltfirp 39293 sge0reuzb 39341 iundjiun 39353 ovnlerp 39452 smflimlem4 39660 2reurex 39830 |
Copyright terms: Public domain | W3C validator |