![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > rspc2ev | Structured version Visualization version Unicode version |
Description: 2-variable restricted existential specialization, using implicit substitution. (Contributed by NM, 16-Oct-1999.) |
Ref | Expression |
---|---|
rspc2v.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
rspc2v.2 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
rspc2ev |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | rspc2v.2 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | rspcev 3161 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | 2 | anim2i 577 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | 3 | 3impb 1211 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | rspc2v.1 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
6 | 5 | rexbidv 2912 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
7 | 6 | rspcev 3161 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
8 | 4, 7 | syl 17 |
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 1679 ax-4 1692 ax-5 1768 ax-6 1815 ax-7 1861 ax-10 1925 ax-11 1930 ax-12 1943 ax-13 2101 ax-ext 2441 |
This theorem depends on definitions: df-bi 190 df-an 377 df-3an 993 df-tru 1457 df-ex 1674 df-nf 1678 df-sb 1808 df-clab 2448 df-cleq 2454 df-clel 2457 df-nfc 2591 df-rex 2754 df-v 3058 |
This theorem is referenced by: rspc3ev 3174 opelxp 4882 f1prex 6206 rspceov 6353 erov 7485 ralxpmap 7546 2dom 7667 elfiun 7969 dffi3 7970 ixpiunwdom 8131 1re 9667 wrdl2exs2 13070 ello12r 13629 ello1d 13635 elo12r 13640 o1lo1 13649 addcn2 13705 mulcn2 13707 bezoutlem3OLD 14553 bezoutlem3 14556 bezout 14558 pythagtriplem18 14830 pczpre 14845 pcdiv 14850 4sqlem3 14942 4sqlem4 14944 4sqlem12 14948 vdwlem1 14979 vdwlem6 14984 vdwlem8 14986 vdwlem12 14990 vdwlem13 14991 0ram 15026 ramz2 15030 sgrp2rid2ex 16709 pmtr3ncom 17164 psgnunilem1 17182 irredn0 17979 isnzr2 18535 hausnei2 20417 cnhaus 20418 dishaus 20446 ordthauslem 20447 txuni2 20628 xkoopn 20652 txopn 20665 txdis 20695 txdis1cn 20698 pthaus 20701 txhaus 20710 tx1stc 20713 xkohaus 20716 regr1lem 20802 qustgplem 21183 methaus 21583 met2ndci 21585 metnrmlem3 21926 metnrmlem3OLD 21941 elplyr 23203 aaliou2b 23345 aaliou3lem9 23354 2sqlem2 24340 2sqlem8 24348 2sqlem11 24351 2sqb 24354 pntibnd 24479 legov 24678 iscgrad 24901 f1otrge 24950 axsegconlem1 24995 axsegcon 25005 axpaschlem 25018 axlowdimlem6 25025 axlowdim1 25037 axlowdim2 25038 axeuclidlem 25040 el2wlksotot 25658 3cyclfrgrarn1 25788 4cycl2vnunb 25793 br8d 28266 lt2addrd 28374 xlt2addrd 28386 xrnarchi 28549 txomap 28709 tpr2rico 28766 qqhval2 28834 elsx 29064 isanmbfm 29126 br2base 29139 dya2iocnrect 29151 conpcon 30006 br8 30444 br4 30446 fprb 30461 brsegle 30923 hilbert1.1 30969 nn0prpwlem 31026 poimirlem1 31985 itg2addnclem3 32039 cntotbnd 32172 smprngopr 32329 3dim2 33077 llni2 33121 lvoli3 33186 lvoli2 33190 islinei 33349 psubspi2N 33357 elpaddri 33411 eldioph2lem1 35646 diophin 35659 fphpdo 35704 irrapxlem3 35712 irrapxlem4 35713 pellexlem6 35722 pell1234qrreccl 35744 pell1234qrmulcl 35745 pell1234qrdich 35751 pell1qr1 35761 pellqrexplicit 35767 rmxycomplete 35809 dgraalem 36051 dgraalemOLD 36052 fourierdlem64 38071 rspceaov 38736 6gbe 38909 7gbo 38910 8gbe 38911 9gboa 38912 11gboa 38913 structgrssvtxlem 39170 upgredg 39275 upgr4cycl4dv4e 39925 usgvad2edg 39995 modn0mul 40595 elbigo2r 40636 |
Copyright terms: Public domain | W3C validator |