![]() |
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 3166 | . 2 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 (𝜓 → 𝜒)) |
4 | rexim 3188 | . 2 ⊢ (∀𝑥 ∈ 𝐴 (𝜓 → 𝜒) → (∃𝑥 ∈ 𝐴 𝜓 → ∃𝑥 ∈ 𝐴 𝜒)) | |
5 | 3, 4 | syl 17 | 1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → ∃𝑥 ∈ 𝐴 𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 Ⅎwnf 1746 ∈ wcel 2050 ∀wral 3088 ∃wrex 3089 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1758 ax-4 1772 ax-5 1869 ax-6 1928 ax-7 1965 ax-12 2106 |
This theorem depends on definitions: df-bi 199 df-an 388 df-ex 1743 df-nf 1747 df-ral 3093 df-rex 3094 |
This theorem is referenced by: 2reurex 3661 tz7.49 7886 hsmexlem2 9649 acunirnmpt2 30170 acunirnmpt2f 30171 locfinreflem 30748 cmpcref 30758 fvineqsneq 34134 indexdom 34451 filbcmb 34457 cdlemefr29exN 36983 rexanuz3 40785 reximdd 40844 disjrnmpt2 40874 fompt 40878 disjinfi 40879 iunmapsn 40906 infnsuprnmpt 40951 rnmptbdlem 40956 supxrge 41036 suplesup 41037 infxr 41065 allbutfi 41096 supxrunb3 41103 infxrunb3rnmpt 41134 infrpgernmpt 41173 limsupre 41354 limsupub 41417 limsupre3lem 41445 limsupgtlem 41490 xlimmnfvlem1 41545 xlimpnfvlem1 41549 stoweidlem31 41748 stoweidlem34 41751 fourierdlem73 41896 sge0pnffigt 42110 sge0ltfirp 42114 sge0reuzb 42162 iundjiun 42174 ovnlerp 42276 smflimlem4 42482 smflimsuplem7 42532 |
Copyright terms: Public domain | W3C validator |