![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > ralrn | Structured version Visualization version Unicode version |
Description: Restricted universal quantification over the range of a function. (Contributed by Mario Carneiro, 24-Dec-2013.) (Revised by Mario Carneiro, 20-Aug-2014.) |
Ref | Expression |
---|---|
rexrn.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
ralrn |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | fvex 5898 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | a1i 11 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | fvelrnb 5935 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | eqcom 2469 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
5 | 4 | rexbii 2901 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
6 | 3, 5 | syl6bb 269 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
7 | rexrn.1 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
8 | 7 | adantl 472 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
9 | 2, 6, 8 | ralxfr2d 4630 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1680 ax-4 1693 ax-5 1769 ax-6 1816 ax-7 1862 ax-9 1907 ax-10 1926 ax-11 1931 ax-12 1944 ax-13 2102 ax-ext 2442 ax-sep 4539 ax-nul 4548 ax-pr 4653 |
This theorem depends on definitions: df-bi 190 df-or 376 df-an 377 df-3an 993 df-tru 1458 df-ex 1675 df-nf 1679 df-sb 1809 df-eu 2314 df-mo 2315 df-clab 2449 df-cleq 2455 df-clel 2458 df-nfc 2592 df-ne 2635 df-ral 2754 df-rex 2755 df-rab 2758 df-v 3059 df-sbc 3280 df-dif 3419 df-un 3421 df-in 3423 df-ss 3430 df-nul 3744 df-if 3894 df-sn 3981 df-pr 3983 df-op 3987 df-uni 4213 df-br 4417 df-opab 4476 df-mpt 4477 df-id 4768 df-xp 4859 df-rel 4860 df-cnv 4861 df-co 4862 df-dm 4863 df-rn 4864 df-iota 5565 df-fun 5603 df-fn 5604 df-fv 5609 |
This theorem is referenced by: ralrnmpt 6054 cbvfo 6212 isoselem 6257 indexfi 7908 ordtypelem9 8067 ordtypelem10 8068 wemapwe 8228 numacn 8506 acndom 8508 rpnnen1lem3 11321 fsequb2 12221 limsuple 13585 limsupleOLD 13586 limsupval2 13589 limsupval2OLD 13590 climsup 13782 ruclem11 14341 ruclem12 14342 prmreclem6 14914 imasaddfnlem 15483 imasvscafn 15492 cycsubgcl 16892 ghmrn 16945 ghmnsgima 16955 pgpssslw 17315 gexex 17540 dprdfcntz 17697 znf1o 19171 frlmlbs 19404 lindfrn 19428 ptcnplem 20685 kqt0lem 20800 isr0 20801 regr1lem2 20804 uzrest 20961 tmdgsum2 21160 imasf1oxmet 21439 imasf1omet 21440 bndth 22035 evth 22036 ovolficcss 22471 ovollb2lem 22490 ovolunlem1 22499 ovoliunlem1 22504 ovoliunlem2 22505 ovoliun2 22508 ovolscalem1 22515 ovolicc1 22518 voliunlem2 22553 voliunlem3 22554 ioombl1lem4 22563 uniioovol 22585 uniioombllem2 22589 uniioombllem2OLD 22590 uniioombllem3 22592 uniioombllem6 22595 volsup2 22612 vitalilem3 22617 mbfsup 22669 mbfinf 22670 mbfinfOLD 22671 mbflimsup 22672 mbflimsupOLD 22673 itg1ge0 22693 itg1mulc 22711 itg1climres 22721 mbfi1fseqlem4 22725 itg2seq 22749 itg2monolem1 22757 itg2mono 22760 itg2i1fseq2 22763 itg2gt0 22767 itg2cnlem1 22768 itg2cn 22770 limciun 22898 plycpn 23291 hmopidmchi 27853 hmopidmpji 27854 rge0scvg 28804 mclsax 30256 mblfinlem2 32023 ismtyhmeolem 32181 nacsfix 35599 fnwe2lem2 35954 climinf 37722 climinfOLD 37723 |
Copyright terms: Public domain | W3C validator |