![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > r19.29 | Structured version Visualization version GIF version |
Description: Restricted quantifier version of 19.29 1877. See also r19.29r 3117. (Contributed by NM, 31-Aug-1999.) (Proof shortened by Andrew Salmon, 30-May-2011.) (Proof shortened by Wolf Lammen, 22-Dec-2024.) |
Ref | Expression |
---|---|
r19.29 | ⊢ ((∀𝑥 ∈ 𝐴 𝜑 ∧ ∃𝑥 ∈ 𝐴 𝜓) → ∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ibar 530 | . . 3 ⊢ (𝜑 → (𝜓 ↔ (𝜑 ∧ 𝜓))) | |
2 | 1 | ralrexbid 3107 | . 2 ⊢ (∀𝑥 ∈ 𝐴 𝜑 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓))) |
3 | 2 | biimpa 478 | 1 ⊢ ((∀𝑥 ∈ 𝐴 𝜑 ∧ ∃𝑥 ∈ 𝐴 𝜓) → ∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 397 ∀wral 3062 ∃wrex 3071 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 |
This theorem depends on definitions: df-bi 206 df-an 398 df-ex 1783 df-ral 3063 df-rex 3072 |
This theorem is referenced by: r19.29rOLD 3118 2r19.29 3140 r19.29d2rOLD 3142 disjiun 5131 triun 5276 ralxfrd 5402 ralxfrd2 5406 elrnmptg 5953 fmpt 7097 fliftfun 7296 fiunlem 7915 fiun 7916 f1iun 7917 omabs 8638 findcard3 9273 findcard3OLD 9274 r1sdom 9756 tcrank 9866 infxpenlem 9995 dfac12k 10129 cfslb2n 10250 cfcoflem 10254 iundom2g 10522 supsrlem 11093 axpre-sup 11151 fimaxre3 12147 hashgt23el 14371 limsupbnd2 15414 rlimuni 15481 rlimcld2 15509 rlimno1 15587 pgpfac1lem5 19932 rhmdvdsr 20265 ppttop 22479 epttop 22481 tgcnp 22726 lmcnp 22777 bwth 22883 1stcrest 22926 txlm 23121 tx1stc 23123 fbfinnfr 23314 fbunfip 23342 filuni 23358 ufileu 23392 fbflim2 23450 flftg 23469 ufilcmp 23505 cnpfcf 23514 tsmsxp 23628 metss 23986 lmmbr 24744 ivthlem2 24938 ivthlem3 24939 dyadmax 25084 tpr2rico 32823 esumpcvgval 33007 sigaclcuni 33047 voliune 33158 volfiniune 33159 dya2icoseg2 33208 umgr2cycllem 34062 umgr2cycl 34063 poimirlem29 36422 unirep 36487 heibor1lem 36583 pmapglbx 38546 stoweidlem35 44624 |
Copyright terms: Public domain | W3C validator |