![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > brrelexi | Structured version Visualization version Unicode version |
Description: The first argument of a binary relation exists. (An artifact of our ordered pair definition.) (Contributed by NM, 4-Jun-1998.) |
Ref | Expression |
---|---|
brrelexi.1 |
![]() ![]() ![]() |
Ref | Expression |
---|---|
brrelexi |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | brrelexi.1 |
. 2
![]() ![]() ![]() | |
2 | brrelex 4892 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | mpan 681 |
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-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-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-br 4417 df-opab 4476 df-xp 4859 df-rel 4860 |
This theorem is referenced by: nprrel 4896 vtoclr 4898 opeliunxp2 4992 ideqg 5005 issetid 5008 dffv2 5961 brrpssg 6600 opeliunxp2f 6983 brtpos2 7005 brdomg 7605 isfi 7619 en1uniel 7667 domdifsn 7681 undom 7686 xpdom2 7693 xpdom1g 7695 sbth 7718 dom0 7726 sdom0 7730 sdomirr 7735 sdomdif 7746 fodomr 7749 pwdom 7750 xpen 7761 pwen 7771 php3 7784 sucdom2 7794 sdom1 7798 fineqv 7813 f1finf1o 7824 infsdomnn 7858 relprcnfsupp 7912 fsuppimp 7915 fsuppunbi 7930 mapfien2 7948 harword 8106 brwdom 8108 domwdom 8115 brwdom3i 8124 unwdomg 8125 xpwdomg 8126 infdifsn 8188 ac10ct 8491 inffien 8520 iunfictbso 8571 cdaen 8629 cdadom1 8642 cdafi 8646 cdainflem 8647 cdalepw 8652 unctb 8661 infcdaabs 8662 infunabs 8663 infmap2 8674 cfslb2n 8724 fin4i 8754 isfin5 8755 isfin6 8756 fin4en1 8765 isfin4-3 8771 isfin32i 8821 fin45 8848 fin56 8849 fin67 8851 hsmexlem1 8882 hsmexlem3 8884 axcc3 8894 ttukeylem1 8965 brdom3 8982 iundom2g 8991 iundom 8993 iunctb 9025 gchi 9075 engch 9079 gchdomtri 9080 fpwwe2lem6 9086 fpwwe2lem7 9087 fpwwe2lem9 9089 gchpwdom 9121 prcdnq 9444 reexALT 11325 hasheni 12563 hashdomi 12591 brfi1indALT 12686 climcl 13612 climi 13623 climrlim2 13660 climrecl 13696 climge0 13697 iseralt 13800 climfsum 13929 strfv 15206 issubc 15789 pmtrfv 17142 dprdval 17684 cnfldex 19022 frgpcyg 19193 lindff 19422 lindfind 19423 f1lindf 19429 lindfmm 19434 lsslindf 19437 lbslcic 19448 cctop 20070 1stcrestlem 20516 2ndcdisj2 20521 dis2ndc 20524 hauspwdom 20565 refbas 20574 refssex 20575 reftr 20578 refun0 20579 ovoliunnul 22509 uniiccdif 22584 dvle 23008 uhgrav 25072 ushgraf 25078 ushgrauhgra 25079 umgraf2 25093 umgrares 25100 umisuhgra 25103 uslgrav 25113 usgrav 25114 uslgraf 25121 iscusgra0 25234 eupap1 25753 eupath2lem3 25756 eupath2 25757 frisusgrapr 25768 isrngo 26155 isdivrngo 26208 hlimi 26890 brsset 30705 brbigcup 30714 elfix2 30720 brcolinear2 30874 isfne 31044 refssfne 31063 ovoliunnfl 32027 voliunnfl 32029 volsupnfl 32030 brabg2 32087 heiborlem4 32191 fphpd 35704 ctbnfien 35706 rlimdmafv 38717 subgrv 39392 linindsv 40511 |
Copyright terms: Public domain | W3C validator |