![]() |
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 1916. (Contributed by NM, 28-Jan-1997.) (Proof shortened by Andrew Salmon, 30-May-2011.) |
Ref | Expression |
---|---|
r19.26 | ⊢ (∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ (∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐴 𝜓)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simpl 476 | . . . 4 ⊢ ((𝜑 ∧ 𝜓) → 𝜑) | |
2 | 1 | ralimi 3134 | . . 3 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) → ∀𝑥 ∈ 𝐴 𝜑) |
3 | simpr 479 | . . . 4 ⊢ ((𝜑 ∧ 𝜓) → 𝜓) | |
4 | 3 | ralimi 3134 | . . 3 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) → ∀𝑥 ∈ 𝐴 𝜓) |
5 | 2, 4 | jca 507 | . 2 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) → (∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐴 𝜓)) |
6 | pm3.2 463 | . . . 4 ⊢ (𝜑 → (𝜓 → (𝜑 ∧ 𝜓))) | |
7 | 6 | ral2imi 3129 | . . 3 ⊢ (∀𝑥 ∈ 𝐴 𝜑 → (∀𝑥 ∈ 𝐴 𝜓 → ∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓))) |
8 | 7 | imp 397 | . 2 ⊢ ((∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐴 𝜓) → ∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓)) |
9 | 5, 8 | impbii 201 | 1 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ (∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐴 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 198 ∧ wa 386 ∀wral 3090 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1839 ax-4 1853 |
This theorem depends on definitions: df-bi 199 df-an 387 df-ral 3095 |
This theorem is referenced by: r19.26-2 3251 r19.26-3 3252 ralbiim 3255 r19.27v 3256 r19.35 3270 reu8 3614 ssrab 3901 r19.28z 4286 r19.27z 4293 ralnralall 4301 2ralunsn 4660 iuneq2 4772 disjxun 4886 triin 5004 asymref2 5770 cnvpo 5929 fncnv 6209 fnres 6255 mptfnf 6263 fnopabg 6265 mpteqb 6562 eqfnfv3 6578 fvn0ssdmfun 6616 caoftrn 7211 wfr3g 7697 iiner 8104 ixpeq2 8210 ixpin 8221 ixpfi2 8554 wemaplem2 8743 dfac5 9286 kmlem6 9314 eltsk2g 9910 intgru 9973 axgroth6 9987 fsequb 13097 rexanuz 14496 rexanre 14497 cau3lem 14505 rlimcn2 14733 o1of2 14755 o1rlimmul 14761 climbdd 14814 sqrt2irr 15386 gcdcllem1 15631 pc11 15992 prmreclem2 16029 catpropd 16758 issubc3 16898 fucinv 17022 ispos2 17338 issubg3 18000 issubg4 18001 pmtrdifwrdel2 18293 ringsrg 18980 cply1mul 20064 iunocv 20428 scmatf1 20746 cpmatsubgpmat 20936 tgval2 21172 1stcelcls 21677 ptclsg 21831 ptcnplem 21837 fbun 22056 txflf 22222 ucncn 22501 prdsmet 22587 metequiv 22726 metequiv2 22727 ncvsi 23362 iscau4 23489 cmetcaulem 23498 evthicc2 23668 ismbfcn 23837 mbfi1flimlem 23930 rolle 24194 itgsubst 24253 plydivex 24493 ulmcaulem 24589 ulmcau 24590 ulmbdd 24593 ulmcn 24594 mumullem2 25362 2sqlem6 25604 tgcgr4 25886 axpasch 26294 axeuclid 26316 axcontlem2 26318 axcontlem4 26320 axcontlem7 26323 vtxd0nedgb 26840 fusgrregdegfi 26921 rusgr1vtxlem 26939 uspgr2wlkeq 26997 wlkdlem4 27040 lfgriswlk 27043 frgrreg 27830 frgrregord013 27831 friendshipgt3 27834 ocsh 28718 spanuni 28979 riesz4i 29498 leopadd 29567 leoptri 29571 leoptr 29572 disjunsn 29974 voliune 30894 volfiniune 30895 eulerpartlemr 31038 eulerpartlemn 31045 dfpo2 32243 poseq 32346 wzel 32362 frr3g 32372 ssltun2 32509 neibastop1 32946 phpreu 34023 ptrecube 34040 poimirlem23 34063 poimirlem27 34067 ovoliunnfl 34082 voliunnfl 34084 volsupnfl 34085 itg2addnc 34094 inixp 34153 rngoueqz 34368 intidl 34457 pclclN 36050 tendoeq2 36933 mzpincl 38267 lerabdioph 38339 ltrabdioph 38342 nerabdioph 38343 dvdsrabdioph 38344 dford3lem1 38562 gneispace 39398 ssrabf 40237 climxrre 40900 stoweidlem7 41161 stoweidlem54 41208 dirkercncflem3 41259 2ralbiim 42143 2reu4a 42160 ply1mulgsumlem1 43199 ldepsnlinclem1 43319 ldepsnlinclem2 43320 |
Copyright terms: Public domain | W3C validator |