Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > elpri | Unicode version |
Description: If a class is an element of a pair, then it is one of the two paired elements. (Contributed by Scott Fenton, 1-Apr-2011.) |
Ref | Expression |
---|---|
elpri |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elprg 3542 | . 2 | |
2 | 1 | ibi 175 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wo 697 wceq 1331 wcel 1480 cpr 3523 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-io 698 ax-5 1423 ax-7 1424 ax-gen 1425 ax-ie1 1469 ax-ie2 1470 ax-8 1482 ax-10 1483 ax-11 1484 ax-i12 1485 ax-bndl 1486 ax-4 1487 ax-17 1506 ax-i9 1510 ax-ial 1514 ax-i5r 1515 ax-ext 2119 |
This theorem depends on definitions: df-bi 116 df-tru 1334 df-nf 1437 df-sb 1736 df-clab 2124 df-cleq 2130 df-clel 2133 df-nfc 2268 df-v 2683 df-un 3070 df-sn 3528 df-pr 3529 |
This theorem is referenced by: nelpri 3546 nelprd 3548 opth1 4153 0nelop 4165 ontr2exmid 4435 onintexmid 4482 reg3exmidlemwe 4488 funtpg 5169 ftpg 5597 acexmidlemcase 5762 2oconcl 6329 en2eqpr 6794 eldju1st 6949 finomni 7005 exmidomniim 7006 ismkvnex 7022 exmidonfinlem 7042 exmidfodomrlemr 7051 exmidfodomrlemrALT 7052 exmidaclem 7057 sup3exmid 8708 m1expcl2 10308 maxleim 10970 maxleast 10978 zmaxcl 10989 minmax 10994 xrmaxleim 11006 xrmaxaddlem 11022 xrminmax 11027 unct 11943 qtopbas 12680 limcimolemlt 12791 recnprss 12814 coseq0negpitopi 12906 el2oss1o 13177 nninfalllem1 13192 nninfall 13193 nninfsellemqall 13200 nninfomnilem 13203 isomninnlem 13214 trilpolemclim 13218 trilpolemcl 13219 trilpolemisumle 13220 trilpolemeq1 13222 trilpolemlt1 13223 |
Copyright terms: Public domain | W3C validator |