| 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 1870. (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 3083 | . . 3 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) → ∀𝑥 ∈ 𝐴 𝜑) |
| 3 | simpr 484 | . . . 4 ⊢ ((𝜑 ∧ 𝜓) → 𝜓) | |
| 4 | 3 | ralimi 3083 | . . 3 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) → ∀𝑥 ∈ 𝐴 𝜓) |
| 5 | 2, 4 | jca 511 | . 2 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) → (∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐴 𝜓)) |
| 6 | pm3.2 469 | . . . 4 ⊢ (𝜑 → (𝜓 → (𝜑 ∧ 𝜓))) | |
| 7 | 6 | ral2imi 3085 | . . 3 ⊢ (∀𝑥 ∈ 𝐴 𝜑 → (∀𝑥 ∈ 𝐴 𝜓 → ∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓))) |
| 8 | 7 | imp 406 | . 2 ⊢ ((∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐴 𝜓) → ∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓)) |
| 9 | 5, 8 | impbii 209 | 1 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ (∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐴 𝜓)) |
| Colors of variables: wff setvar class |
| Syntax hints: ↔ wb 206 ∧ wa 395 ∀wral 3061 |
| 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-ral 3062 |
| This theorem is referenced by: r19.26-3 3112 ralbiim 3113 2ralbiim 3132 r19.26-2 3138 r19.27v 3188 r19.28v 3190 reu8 3739 ssrab 4073 r19.28z 4498 r19.27z 4505 ralf0 4514 ralnralall 4515 2reu4lem 4522 2ralunsn 4895 iuneq2 5011 disjxun 5141 triin 5276 asymref2 6137 cnvpo 6307 dfpo2 6316 fncnv 6639 fnres 6695 mptfnf 6703 fnopabg 6705 mpteqb 7035 eqfnfv3 7053 fvn0ssdmfun 7094 caoftrn 7738 poseq 8183 wfr3g 8347 iiner 8829 ixpeq2 8951 ixpin 8963 ixpfi2 9390 wemaplem2 9587 frr3g 9796 dfac5 10169 kmlem6 10196 eltsk2g 10791 intgru 10854 axgroth6 10868 fsequb 14016 rexanuz 15384 rexanre 15385 cau3lem 15393 rlimcn3 15626 o1of2 15649 o1rlimmul 15655 climbdd 15708 sqrt2irr 16285 gcdcllem1 16536 pc11 16918 prmreclem2 16955 catpropd 17752 issubc3 17894 fucinv 18021 ispos2 18361 issubg3 19162 issubg4 19163 pmtrdifwrdel2 19504 ringsrg 20294 iunocv 21699 cply1mul 22300 scmatf1 22537 cpmatsubgpmat 22726 tgval2 22963 1stcelcls 23469 ptclsg 23623 ptcnplem 23629 fbun 23848 txflf 24014 ucncn 24294 prdsmet 24380 metequiv 24522 metequiv2 24523 ncvsi 25185 iscau4 25313 cmetcaulem 25322 evthicc2 25495 ismbfcn 25664 mbfi1flimlem 25757 rolle 26028 itgsubst 26090 plydivex 26339 ulmcaulem 26437 ulmcau 26438 ulmbdd 26441 ulmcn 26442 mumullem2 27223 2sqlem6 27467 tgcgr4 28539 axpasch 28956 axeuclid 28978 axcontlem2 28980 axcontlem4 28982 axcontlem7 28985 vtxd0nedgb 29506 fusgrregdegfi 29587 rusgr1vtxlem 29605 uspgr2wlkeq 29664 wlkdlem4 29703 lfgriswlk 29706 frgrreg 30413 frgrregord013 30414 friendshipgt3 30417 ocsh 31302 spanuni 31563 riesz4i 32082 leopadd 32151 leoptri 32155 leoptr 32156 inpr0 32550 disjunsn 32607 voliune 34230 volfiniune 34231 eulerpartlemr 34376 eulerpartlemn 34383 nummin 35105 fmlasucdisj 35404 wzel 35825 neibastop1 36360 numiunnum 36471 phpreu 37611 ptrecube 37627 poimirlem23 37650 poimirlem27 37654 ovoliunnfl 37669 voliunnfl 37671 volsupnfl 37672 itg2addnc 37681 inixp 37735 rngoueqz 37947 intidl 38036 pclclN 39893 tendoeq2 40776 deg1gprod 42141 mzpincl 42745 lerabdioph 42816 ltrabdioph 42819 nerabdioph 42820 dvdsrabdioph 42821 dford3lem1 43038 gneispace 44147 ssrabf 45119 r19.28zf 45164 climxrre 45765 stoweidlem7 46022 stoweidlem54 46069 dirkercncflem3 46120 ply1mulgsumlem1 48303 ldepsnlinclem1 48422 ldepsnlinclem2 48423 |
| Copyright terms: Public domain | W3C validator |