![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > r19.29r | Structured version Visualization version GIF version |
Description: Restricted quantifier version of 19.29r 1875; variation of r19.29 3216. (Contributed by NM, 31-Aug-1999.) (Proof shortened by Wolf Lammen, 29-Jun-2023.) |
Ref | Expression |
---|---|
r19.29r | ⊢ ((∃𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐴 𝜓) → ∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | r19.29 3216 | . . 3 ⊢ ((∀𝑥 ∈ 𝐴 𝜓 ∧ ∃𝑥 ∈ 𝐴 𝜑) → ∃𝑥 ∈ 𝐴 (𝜓 ∧ 𝜑)) | |
2 | 1 | ancoms 462 | . 2 ⊢ ((∃𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐴 𝜓) → ∃𝑥 ∈ 𝐴 (𝜓 ∧ 𝜑)) |
3 | pm3.22 463 | . . 3 ⊢ ((𝜓 ∧ 𝜑) → (𝜑 ∧ 𝜓)) | |
4 | 3 | reximi 3206 | . 2 ⊢ (∃𝑥 ∈ 𝐴 (𝜓 ∧ 𝜑) → ∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓)) |
5 | 2, 4 | syl 17 | 1 ⊢ ((∃𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐴 𝜓) → ∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 399 ∀wral 3106 ∃wrex 3107 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 |
This theorem depends on definitions: df-bi 210 df-an 400 df-ex 1782 df-ral 3111 df-rex 3112 |
This theorem is referenced by: r19.29imd 3218 2reu5 3697 rlimuni 14899 rlimno1 15002 neindisj2 21728 lmss 21903 fclsbas 22626 isfcf 22639 ucnima 22887 metcnp3 23147 cfilucfil 23166 bndth 23563 ellimc3 24482 lmxrge0 31305 gsumesum 31428 esumcst 31432 esumfsup 31439 voliune 31598 volfiniune 31599 bnj517 32267 nummin 32474 fvineqsneq 34829 cover2 35152 prmunb2 41015 |
Copyright terms: Public domain | W3C validator |