Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > r19.29 | Structured version Visualization version Unicode version |
Description: Restricted quantifier version of 19.29 1801. See also r19.29r 3073. (Contributed by NM, 31-Aug-1999.) (Proof shortened by Andrew Salmon, 30-May-2011.) |
Ref | Expression |
---|---|
r19.29 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pm3.2 463 | . . . 4 | |
2 | 1 | ralimi 2952 | . . 3 |
3 | rexim 3008 | . . 3 | |
4 | 2, 3 | syl 17 | . 2 |
5 | 4 | imp 445 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wi 4 wa 384 wral 2912 wrex 2913 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 |
This theorem depends on definitions: df-bi 197 df-an 386 df-ex 1705 df-ral 2917 df-rex 2918 |
This theorem is referenced by: r19.29r 3073 2r19.29 3079 r19.29d2r 3080 disjiun 4640 triun 4766 ralxfrd 4879 ralxfrdOLD 4880 ralxfrd2 4884 elrnmptg 5375 fmpt 6381 fliftfun 6562 fun11iun 7126 omabs 7727 findcard3 8203 r1sdom 8637 tcrank 8747 infxpenlem 8836 dfac12k 8969 cfslb2n 9090 cfcoflem 9094 iundom2g 9362 supsrlem 9932 axpre-sup 9990 fimaxre3 10970 limsupbnd2 14214 rlimuni 14281 rlimcld2 14309 rlimno1 14384 pgpfac1lem5 18478 ppttop 20811 epttop 20813 tgcnp 21057 lmcnp 21108 bwth 21213 1stcrest 21256 txlm 21451 tx1stc 21453 fbfinnfr 21645 fbunfip 21673 filuni 21689 ufileu 21723 fbflim2 21781 flftg 21800 ufilcmp 21836 cnpfcf 21845 tsmsxp 21958 metss 22313 lmmbr 23056 ivthlem2 23221 ivthlem3 23222 dyadmax 23366 rhmdvdsr 29818 tpr2rico 29958 esumpcvgval 30140 sigaclcuni 30181 voliune 30292 volfiniune 30293 dya2icoseg2 30340 poimirlem29 33438 unirep 33507 heibor1lem 33608 pmapglbx 35055 stoweidlem35 40252 |
Copyright terms: Public domain | W3C validator |