![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > elpri | Structured version Visualization version 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 3996 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | ibi 249 |
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-10 1926 ax-11 1931 ax-12 1944 ax-13 2102 ax-ext 2442 |
This theorem depends on definitions: df-bi 190 df-or 376 df-an 377 df-tru 1458 df-ex 1675 df-nf 1679 df-sb 1809 df-clab 2449 df-cleq 2455 df-clel 2458 df-nfc 2592 df-v 3059 df-un 3421 df-sn 3981 df-pr 3983 |
This theorem is referenced by: elpr2 3999 nelpri 4000 nelprd 4001 tppreqb 4126 elpreqpr 4175 opth1 4692 0nelop 4708 funtpg 5655 ftpg 6103 2oconcl 7236 cantnflem2 8226 m1expcl2 12332 hash2pwpr 12674 bitsinv1lem 14470 xpscfv 15523 xpsfeq 15525 pmtrprfval 17183 m1expaddsub 17194 psgnprfval 17217 frgpuptinv 17476 frgpup3lem 17482 cnmsgnsubg 19200 zrhpsgnelbas 19217 mdetralt 19688 m2detleiblem1 19704 indiscld 20162 cnindis 20363 conclo 20485 txindis 20704 xpsxmetlem 21449 xpsmet 21452 ishl2 22392 recnprss 22915 recnperf 22916 dvlip2 23003 coseq0negpitopi 23514 pythag 23802 reasinsin 23878 scvxcvx 23967 perfectlem2 24214 lgslem4 24283 lgseisenlem2 24334 usgraedg4 25170 cusgrares 25256 2pthlem2 25382 vdgr1a 25690 konigsberg 25771 ex-pr 25936 elpreq 28212 1neg1t1neg1 28377 signswch 29500 kur14lem7 29985 poimirlem31 32017 ftc1anclem2 32064 wepwsolem 35946 relexp01min 36351 ssrecnpr 36701 seff 36702 sblpnf 36703 expgrowthi 36727 dvconstbi 36728 sumpair 37397 refsum2cnlem1 37399 iooinlbub 37683 elprn1 37799 elprn2 37800 cncfiooicclem1 37857 dvmptconst 37871 dvmptidg 37873 dvmulcncf 37883 dvdivcncf 37885 elprneb 38847 perfectALTVlem2 38979 elpr2elpr 39140 usgredg4 39440 usgvincvad 40085 usgvincvadALT 40088 0dig2pr01 40790 |
Copyright terms: Public domain | W3C validator |