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 3213 | . 2 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 (𝜓 → 𝜒)) |
4 | rexim 3238 | . 2 ⊢ (∀𝑥 ∈ 𝐴 (𝜓 → 𝜒) → (∃𝑥 ∈ 𝐴 𝜓 → ∃𝑥 ∈ 𝐴 𝜒)) | |
5 | 3, 4 | syl 17 | 1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → ∃𝑥 ∈ 𝐴 𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 Ⅎwnf 1775 ∈ wcel 2105 ∀wral 3135 ∃wrex 3136 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-12 2167 |
This theorem depends on definitions: df-bi 208 df-an 397 df-ex 1772 df-nf 1776 df-ral 3140 df-rex 3141 |
This theorem is referenced by: 2reurex 3747 tz7.49 8070 hsmexlem2 9837 acunirnmpt2 30333 acunirnmpt2f 30334 locfinreflem 31003 cmpcref 31013 fvineqsneq 34575 indexdom 34890 filbcmb 34896 cdlemefr29exN 37418 rexanuz3 41239 reximdd 41297 disjrnmpt2 41325 fompt 41329 disjinfi 41330 iunmapsn 41356 infnsuprnmpt 41398 rnmptbdlem 41403 supxrge 41482 suplesup 41483 infxr 41511 allbutfi 41541 supxrunb3 41548 infxrunb3rnmpt 41578 infrpgernmpt 41617 limsupre 41798 limsupub 41861 limsupre3lem 41889 limsupgtlem 41934 xlimmnfvlem1 41989 xlimpnfvlem1 41993 stoweidlem31 42193 stoweidlem34 42196 fourierdlem73 42341 sge0pnffigt 42555 sge0ltfirp 42559 sge0reuzb 42607 iundjiun 42619 ovnlerp 42721 smflimlem4 42927 smflimsuplem7 42977 |
Copyright terms: Public domain | W3C validator |