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 1882; variation of r19.29 3176. (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 3176 | . . 3 ⊢ ((∀𝑥 ∈ 𝐴 𝜓 ∧ ∃𝑥 ∈ 𝐴 𝜑) → ∃𝑥 ∈ 𝐴 (𝜓 ∧ 𝜑)) | |
2 | 1 | ancoms 462 | . 2 ⊢ ((∃𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐴 𝜓) → ∃𝑥 ∈ 𝐴 (𝜓 ∧ 𝜑)) |
3 | pm3.22 463 | . . 3 ⊢ ((𝜓 ∧ 𝜑) → (𝜑 ∧ 𝜓)) | |
4 | 3 | reximi 3166 | . 2 ⊢ (∃𝑥 ∈ 𝐴 (𝜓 ∧ 𝜑) → ∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓)) |
5 | 2, 4 | syl 17 | 1 ⊢ ((∃𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐴 𝜓) → ∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 399 ∀wral 3061 ∃wrex 3062 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 |
This theorem depends on definitions: df-bi 210 df-an 400 df-ex 1788 df-ral 3066 df-rex 3067 |
This theorem is referenced by: r19.29imd 3178 2reu5 3671 rlimuni 15111 rlimno1 15217 neindisj2 22020 lmss 22195 fclsbas 22918 isfcf 22931 ucnima 23178 metcnp3 23438 cfilucfil 23457 bndth 23855 ellimc3 24776 lmxrge0 31616 gsumesum 31739 esumcst 31743 esumfsup 31750 voliune 31909 volfiniune 31910 bnj517 32578 nummin 32776 fvineqsneq 35320 cover2 35609 prmunb2 41602 |
Copyright terms: Public domain | W3C validator |