![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > brrelex1i | Structured version Visualization version GIF 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 | ⊢ Rel 𝑅 |
Ref | Expression |
---|---|
brrelex1i | ⊢ (𝐴𝑅𝐵 → 𝐴 ∈ V) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | brrelexi.1 | . 2 ⊢ Rel 𝑅 | |
2 | brrelex1 5569 | . 2 ⊢ ((Rel 𝑅 ∧ 𝐴𝑅𝐵) → 𝐴 ∈ V) | |
3 | 1, 2 | mpan 689 | 1 ⊢ (𝐴𝑅𝐵 → 𝐴 ∈ V) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2111 Vcvv 3441 class class class wbr 5030 Rel wrel 5524 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2113 ax-9 2121 ax-10 2142 ax-11 2158 ax-12 2175 ax-ext 2770 ax-sep 5167 ax-nul 5174 ax-pr 5295 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 845 df-3an 1086 df-tru 1541 df-ex 1782 df-nf 1786 df-sb 2070 df-clab 2777 df-cleq 2791 df-clel 2870 df-nfc 2938 df-ral 3111 df-rex 3112 df-v 3443 df-dif 3884 df-un 3886 df-in 3888 df-ss 3898 df-nul 4244 df-if 4426 df-sn 4526 df-pr 4528 df-op 4532 df-br 5031 df-opab 5093 df-xp 5525 df-rel 5526 |
This theorem is referenced by: nprrel 5575 opeliunxp2 5673 ideqg 5686 issetid 5689 dffv2 6733 brfvopabrbr 6742 brrpssg 7431 opeliunxp2f 7859 brtpos2 7881 brdomg 8502 ctex 8507 isfi 8516 en1uniel 8564 domdifsn 8583 undom 8588 xpdom2 8595 xpdom1g 8597 sucdom2 8610 sbth 8621 dom0 8629 sdom0 8633 sdomirr 8638 sdomdif 8649 fodomr 8652 pwdom 8653 xpen 8664 pwen 8674 php3 8687 sdom1 8702 fineqv 8717 f1finf1o 8729 infsdomnn 8763 relprcnfsupp 8820 fsuppunbi 8838 mapfien2 8856 harword 9011 brwdom 9015 domwdom 9022 brwdom3i 9031 unwdomg 9032 xpwdomg 9033 infdifsn 9104 ac10ct 9445 inffien 9474 djuen 9580 djudom2 9594 djufi 9597 cdainflem 9598 djulepw 9603 infdjuabs 9617 infunabs 9618 infmap2 9629 cfslb2n 9679 fin4i 9709 isfin5 9710 isfin6 9711 fin4en1 9720 isfin4p1 9726 isfin32i 9776 fin45 9803 fin56 9804 fin67 9806 hsmexlem1 9837 hsmexlem3 9839 axcc3 9849 ttukeylem1 9920 brdom3 9939 iundom2g 9951 iundom 9953 gchi 10035 engch 10039 gchdomtri 10040 fpwwe2lem6 10046 fpwwe2lem7 10047 fpwwe2lem9 10049 gchdjuidm 10079 gchpwdom 10081 prcdnq 10404 reexALT 12371 hasheni 13704 hashdomi 13737 climcl 14848 climi 14859 climrlim2 14896 climrecl 14932 climge0 14933 iseralt 15033 climfsum 15167 structex 16486 issubc 17097 pmtrfv 18572 dprdval 19118 frgpcyg 20265 lindff 20504 lindfind 20505 f1lindf 20511 lindfmm 20516 lsslindf 20519 lbslcic 20530 hauspwdom 22106 refbas 22115 refssex 22116 reftr 22119 refun0 22120 ovoliunnul 24111 dvle 24610 cyclnspth 27589 hlimi 28971 gsumhashmul 30741 extdgval 31132 usgrgt2cycl 32490 brsset 33463 brbigcup 33472 elfix2 33478 brcolinear2 33632 isfne 33800 refssfne 33819 bj-epelg 34484 bj-ideqb 34574 bj-opelidb1ALT 34581 ovoliunnfl 35099 voliunnfl 35101 volsupnfl 35102 brabg2 35154 heiborlem4 35252 isrngo 35335 isdivrngo 35388 brssr 35901 issetssr 35903 fphpd 39757 ctbnfien 39759 climd 42314 climuzlem 42385 rlimdmafv 43733 rlimdmafv2 43814 |
Copyright terms: Public domain | W3C validator |