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 1802; variation of r19.29 3072. (Contributed by NM, 31-Aug-1999.) |
Ref | Expression |
---|---|
r19.29r | ⊢ ((∃𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐴 𝜓) → ∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | r19.29 3072 | . 2 ⊢ ((∀𝑥 ∈ 𝐴 𝜓 ∧ ∃𝑥 ∈ 𝐴 𝜑) → ∃𝑥 ∈ 𝐴 (𝜓 ∧ 𝜑)) | |
2 | ancom 466 | . 2 ⊢ ((∃𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐴 𝜓) ↔ (∀𝑥 ∈ 𝐴 𝜓 ∧ ∃𝑥 ∈ 𝐴 𝜑)) | |
3 | ancom 466 | . . 3 ⊢ ((𝜑 ∧ 𝜓) ↔ (𝜓 ∧ 𝜑)) | |
4 | 3 | rexbii 3041 | . 2 ⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ ∃𝑥 ∈ 𝐴 (𝜓 ∧ 𝜑)) |
5 | 1, 2, 4 | 3imtr4i 281 | 1 ⊢ ((∃𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐴 𝜓) → ∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 384 ∀wral 2912 ∃wrex 2913 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 |
This theorem depends on definitions: df-bi 197 df-an 386 df-ex 1705 df-ral 2917 df-rex 2918 |
This theorem is referenced by: r19.29imd 3074 2reu5 3416 rlimuni 14281 rlimno1 14384 neindisj2 20927 lmss 21102 fclsbas 21825 isfcf 21838 ucnima 22085 metcnp3 22345 cfilucfil 22364 bndth 22757 ellimc3 23643 lmxrge0 29998 gsumesum 30121 esumcst 30125 esumfsup 30132 voliune 30292 volfiniune 30293 bnj517 30955 cover2 33508 prmunb2 38510 |
Copyright terms: Public domain | W3C validator |