| 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 1874; variation of r19.29 3114. (Contributed by NM, 31-Aug-1999.) (Proof shortened by Wolf Lammen, 29-Jun-2023.) |
| Ref | Expression |
|---|---|
| r19.29r | ⊢ ((∃𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐴 𝜓) → ∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓)) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | iba 527 | . . 3 ⊢ (𝜓 → (𝜑 ↔ (𝜑 ∧ 𝜓))) | |
| 2 | 1 | ralrexbid 3106 | . 2 ⊢ (∀𝑥 ∈ 𝐴 𝜓 → (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓))) |
| 3 | 2 | biimpac 478 | 1 ⊢ ((∃𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐴 𝜓) → ∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓)) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∧ wa 395 ∀wral 3061 ∃wrex 3070 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1780 df-ral 3062 df-rex 3071 |
| This theorem is referenced by: r19.29imd 3118 2reu5 3764 rlimuni 15586 rlimno1 15690 neindisj2 23131 lmss 23306 fclsbas 24029 isfcf 24042 ucnima 24290 metcnp3 24553 cfilucfil 24572 bndth 24990 ellimc3 25914 lmxrge0 33951 gsumesum 34060 esumcst 34064 esumfsup 34071 voliune 34230 volfiniune 34231 bnj517 34899 nummin 35105 fvineqsneq 37413 cover2 37722 naddgeoa 43407 prmunb2 44330 |
| Copyright terms: Public domain | W3C validator |