![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > r19.26 | Structured version Visualization version GIF version |
Description: Restricted quantifier version of 19.26 1866. (Contributed by NM, 28-Jan-1997.) (Proof shortened by Andrew Salmon, 30-May-2011.) |
Ref | Expression |
---|---|
r19.26 | ⊢ (∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ (∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐴 𝜓)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simpl 482 | . . . 4 ⊢ ((𝜑 ∧ 𝜓) → 𝜑) | |
2 | 1 | ralimi 3080 | . . 3 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) → ∀𝑥 ∈ 𝐴 𝜑) |
3 | simpr 484 | . . . 4 ⊢ ((𝜑 ∧ 𝜓) → 𝜓) | |
4 | 3 | ralimi 3080 | . . 3 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) → ∀𝑥 ∈ 𝐴 𝜓) |
5 | 2, 4 | jca 511 | . 2 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) → (∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐴 𝜓)) |
6 | pm3.2 469 | . . . 4 ⊢ (𝜑 → (𝜓 → (𝜑 ∧ 𝜓))) | |
7 | 6 | ral2imi 3082 | . . 3 ⊢ (∀𝑥 ∈ 𝐴 𝜑 → (∀𝑥 ∈ 𝐴 𝜓 → ∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓))) |
8 | 7 | imp 406 | . 2 ⊢ ((∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐴 𝜓) → ∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓)) |
9 | 5, 8 | impbii 208 | 1 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ (∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐴 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 205 ∧ wa 395 ∀wral 3058 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 |
This theorem depends on definitions: df-bi 206 df-an 396 df-ral 3059 |
This theorem is referenced by: r19.26-3 3109 ralbiim 3110 2ralbiim 3129 r19.26-2 3135 r19.27v 3184 r19.28v 3186 reu8 3728 ssrab 4068 r19.28z 4498 r19.27z 4505 ralf0 4514 ralnralall 4519 2reu4lem 4526 2ralunsn 4896 iuneq2 5015 disjxun 5146 triin 5282 asymref2 6123 cnvpo 6291 dfpo2 6300 fncnv 6626 fnres 6682 mptfnf 6690 fnopabg 6692 mpteqb 7024 eqfnfv3 7042 fvn0ssdmfun 7084 caoftrn 7723 poseq 8163 wfr3g 8328 iiner 8808 ixpeq2 8930 ixpin 8942 ixpfi2 9375 wemaplem2 9571 frr3g 9780 dfac5 10152 kmlem6 10179 eltsk2g 10775 intgru 10838 axgroth6 10852 fsequb 13973 rexanuz 15325 rexanre 15326 cau3lem 15334 rlimcn3 15567 o1of2 15590 o1rlimmul 15596 climbdd 15651 sqrt2irr 16226 gcdcllem1 16474 pc11 16849 prmreclem2 16886 catpropd 17689 issubc3 17835 fucinv 17965 ispos2 18307 issubg3 19099 issubg4 19100 pmtrdifwrdel2 19441 ringsrg 20233 iunocv 21613 cply1mul 22215 scmatf1 22446 cpmatsubgpmat 22635 tgval2 22872 1stcelcls 23378 ptclsg 23532 ptcnplem 23538 fbun 23757 txflf 23923 ucncn 24203 prdsmet 24289 metequiv 24431 metequiv2 24432 ncvsi 25092 iscau4 25220 cmetcaulem 25229 evthicc2 25402 ismbfcn 25571 mbfi1flimlem 25665 rolle 25935 itgsubst 25997 plydivex 26245 ulmcaulem 26343 ulmcau 26344 ulmbdd 26347 ulmcn 26348 mumullem2 27125 2sqlem6 27369 tgcgr4 28348 axpasch 28765 axeuclid 28787 axcontlem2 28789 axcontlem4 28791 axcontlem7 28794 vtxd0nedgb 29315 fusgrregdegfi 29396 rusgr1vtxlem 29414 uspgr2wlkeq 29473 wlkdlem4 29512 lfgriswlk 29515 frgrreg 30217 frgrregord013 30218 friendshipgt3 30221 ocsh 31106 spanuni 31367 riesz4i 31886 leopadd 31955 leoptri 31959 leoptr 31960 inpr0 32341 disjunsn 32397 voliune 33848 volfiniune 33849 eulerpartlemr 33994 eulerpartlemn 34001 nummin 34714 fmlasucdisj 35009 wzel 35420 neibastop1 35843 phpreu 37077 ptrecube 37093 poimirlem23 37116 poimirlem27 37120 ovoliunnfl 37135 voliunnfl 37137 volsupnfl 37138 itg2addnc 37147 inixp 37201 rngoueqz 37413 intidl 37502 pclclN 39364 tendoeq2 40247 deg1gprod 41612 mzpincl 42154 lerabdioph 42225 ltrabdioph 42228 nerabdioph 42229 dvdsrabdioph 42230 dford3lem1 42447 gneispace 43564 ssrabf 44480 r19.28zf 44530 climxrre 45138 stoweidlem7 45395 stoweidlem54 45442 dirkercncflem3 45493 ply1mulgsumlem1 47454 ldepsnlinclem1 47573 ldepsnlinclem2 47574 |
Copyright terms: Public domain | W3C validator |