![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > relopabi | Structured version Visualization version Unicode version |
Description: A class of ordered pairs is a relation. (Contributed by Mario Carneiro, 21-Dec-2013.) |
Ref | Expression |
---|---|
relopabi.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
relopabi |
![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | relopabi.1 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | df-opab 4475 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | eqtri 2483 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | vex 3059 |
. . . . . . . 8
![]() ![]() ![]() ![]() | |
5 | vex 3059 |
. . . . . . . 8
![]() ![]() ![]() ![]() | |
6 | 4, 5 | opelvv 4899 |
. . . . . . 7
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
7 | eleq1 2527 |
. . . . . . 7
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
8 | 6, 7 | mpbiri 241 |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
9 | 8 | adantr 471 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
10 | 9 | exlimivv 1788 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
11 | 10 | abssi 3515 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
12 | 3, 11 | eqsstri 3473 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
13 | df-rel 4859 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
14 | 12, 13 | mpbir 214 |
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-9 1906 ax-10 1925 ax-11 1930 ax-12 1943 ax-13 2101 ax-ext 2441 ax-sep 4538 ax-nul 4547 ax-pr 4652 |
This theorem depends on definitions: df-bi 190 df-or 376 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-ne 2634 df-ral 2753 df-rex 2754 df-rab 2757 df-v 3058 df-dif 3418 df-un 3420 df-in 3422 df-ss 3429 df-nul 3743 df-if 3893 df-sn 3980 df-pr 3982 df-op 3986 df-opab 4475 df-xp 4858 df-rel 4859 |
This theorem is referenced by: relopab 4978 mptrel 4979 reli 4980 rele 4981 relcnv 5225 cotrg 5229 relco 5351 reloprab 6364 reldmoprab 6407 relrpss 6598 eqer 7421 ecopover 7492 relen 7599 reldom 7600 relfsupp 7910 relwdom 8106 fpwwe2lem2 9082 fpwwe2lem3 9083 fpwwe2lem6 9085 fpwwe2lem7 9086 fpwwe2lem9 9088 fpwwe2lem11 9090 fpwwe2lem12 9091 fpwwe2lem13 9092 fpwwelem 9095 climrel 13604 rlimrel 13605 brstruct 15177 sscrel 15766 gaorber 17010 sylow2a 17319 efgrelexlemb 17448 efgcpbllemb 17453 rellindf 19414 2ndcctbss 20518 refrel 20571 vitalilem1 22614 lgsquadlem1 24330 lgsquadlem2 24331 reluhgra 25069 relushgra 25070 relumgra 25089 reluslgra 25109 relusgra 25110 iscusgra0 25233 cusgrasize 25254 erclwwlkrel 25586 erclwwlknrel 25598 frisusgrapr 25767 relrngo 26153 drngoi 26183 isdivrngo 26207 vcrel 26214 h2hlm 26681 hlimi 26889 relmntop 28876 relae 29111 fnerel 31042 filnetlem3 31084 brabg2 32086 heiborlem3 32189 heiborlem4 32190 isdrngo1 32239 riscer 32271 prter1 32495 prter3 32498 reldvds 36707 relsubgr 39390 relfusgra 40007 rellininds 40508 |
Copyright terms: Public domain | W3C validator |