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 1866; variation of r19.29 3251. (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 3251 | . . 3 ⊢ ((∀𝑥 ∈ 𝐴 𝜓 ∧ ∃𝑥 ∈ 𝐴 𝜑) → ∃𝑥 ∈ 𝐴 (𝜓 ∧ 𝜑)) | |
2 | 1 | ancoms 459 | . 2 ⊢ ((∃𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐴 𝜓) → ∃𝑥 ∈ 𝐴 (𝜓 ∧ 𝜑)) |
3 | pm3.22 460 | . . 3 ⊢ ((𝜓 ∧ 𝜑) → (𝜑 ∧ 𝜓)) | |
4 | 3 | reximi 3240 | . 2 ⊢ (∃𝑥 ∈ 𝐴 (𝜓 ∧ 𝜑) → ∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓)) |
5 | 2, 4 | syl 17 | 1 ⊢ ((∃𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐴 𝜓) → ∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 ∀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 |
This theorem depends on definitions: df-bi 208 df-an 397 df-ex 1772 df-ral 3140 df-rex 3141 |
This theorem is referenced by: r19.29imd 3254 2reu5 3746 rlimuni 14895 rlimno1 14998 neindisj2 21659 lmss 21834 fclsbas 22557 isfcf 22570 ucnima 22817 metcnp3 23077 cfilucfil 23096 bndth 23489 ellimc3 24404 lmxrge0 31094 gsumesum 31217 esumcst 31221 esumfsup 31228 voliune 31387 volfiniune 31388 bnj517 32056 fvineqsneq 34575 cover2 34870 prmunb2 40520 |
Copyright terms: Public domain | W3C validator |