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 1790; variation of r19.29 3054. (Contributed by NM, 31-Aug-1999.) |
Ref | Expression |
---|---|
r19.29r | ⊢ ((∃𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐴 𝜓) → ∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | r19.29 3054 | . 2 ⊢ ((∀𝑥 ∈ 𝐴 𝜓 ∧ ∃𝑥 ∈ 𝐴 𝜑) → ∃𝑥 ∈ 𝐴 (𝜓 ∧ 𝜑)) | |
2 | ancom 465 | . 2 ⊢ ((∃𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐴 𝜓) ↔ (∀𝑥 ∈ 𝐴 𝜓 ∧ ∃𝑥 ∈ 𝐴 𝜑)) | |
3 | ancom 465 | . . 3 ⊢ ((𝜑 ∧ 𝜓) ↔ (𝜓 ∧ 𝜑)) | |
4 | 3 | rexbii 3023 | . 2 ⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ ∃𝑥 ∈ 𝐴 (𝜓 ∧ 𝜑)) |
5 | 1, 2, 4 | 3imtr4i 280 | 1 ⊢ ((∃𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐴 𝜓) → ∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 383 ∀wral 2896 ∃wrex 2897 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 |
This theorem depends on definitions: df-bi 196 df-an 385 df-ex 1696 df-ral 2901 df-rex 2902 |
This theorem is referenced by: r19.29imd 3056 2reu5 3383 rlimuni 14129 rlimno1 14232 neindisj2 20737 lmss 20912 fclsbas 21635 isfcf 21648 ucnima 21895 metcnp3 22155 cfilucfil 22174 bndth 22565 ellimc3 23449 lmxrge0 29326 gsumesum 29448 esumcst 29452 esumfsup 29459 voliune 29619 volfiniune 29620 bnj517 30209 cover2 32678 prmunb2 37532 |
Copyright terms: Public domain | W3C validator |