| 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 5738 | . 2 ⊢ ((Rel 𝑅 ∧ 𝐴𝑅𝐵) → 𝐴 ∈ V) | |
| 3 | 1, 2 | mpan 690 | 1 ⊢ (𝐴𝑅𝐵 → 𝐴 ∈ V) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∈ wcel 2108 Vcvv 3480 class class class wbr 5143 Rel wrel 5690 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-ext 2708 ax-sep 5296 ax-nul 5306 ax-pr 5432 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3an 1089 df-tru 1543 df-fal 1553 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-ral 3062 df-rex 3071 df-rab 3437 df-v 3482 df-dif 3954 df-un 3956 df-ss 3968 df-nul 4334 df-if 4526 df-sn 4627 df-pr 4629 df-op 4633 df-br 5144 df-opab 5206 df-xp 5691 df-rel 5692 |
| This theorem is referenced by: nprrel 5744 opeliunxp2 5849 ideqg 5862 issetid 5865 dffv2 7004 brfvopabrbr 7013 brrpssg 7745 opeliunxp2f 8235 brtpos2 8257 brdomg 8997 brdomgOLD 8998 ctex 9004 isfi 9016 domssr 9039 domdifsn 9094 undomOLD 9100 xpdom2 9107 xpdom1g 9109 sucdom2OLD 9122 sbth 9133 dom0OLD 9143 sdom0OLD 9149 sdomirr 9154 sdomdif 9165 fodomr 9168 pwdom 9169 xpen 9180 pwen 9190 sbthfi 9239 sucdom2 9243 php3OLD 9261 sdom1OLD 9279 fineqv 9299 f1finf1oOLD 9306 infsdomnn 9338 infsdomnnOLD 9339 relprcnfsupp 9404 fsuppssov1 9424 fsuppunbi 9429 mapfien2 9449 harword 9603 brwdom 9607 domwdom 9614 brwdom3i 9623 unwdomg 9624 xpwdomg 9625 infdifsn 9697 ac10ct 10074 inffien 10103 djuen 10210 djudom2 10224 djufi 10227 cdainflem 10228 djulepw 10233 infdjuabs 10245 infunabs 10246 infmap2 10257 cfslb2n 10308 fin4i 10338 isfin5 10339 isfin6 10340 fin4en1 10349 isfin4p1 10355 isfin32i 10405 fin45 10432 fin56 10433 fin67 10435 hsmexlem1 10466 hsmexlem3 10468 axcc3 10478 ttukeylem1 10549 brdom3 10568 iundom2g 10580 iundom 10582 gchi 10664 engch 10668 gchdomtri 10669 fpwwe2lem5 10675 fpwwe2lem6 10676 fpwwe2lem8 10678 gchdjuidm 10708 gchpwdom 10710 prcdnq 11033 reexALT 13026 hasheni 14387 hashdomi 14419 climcl 15535 climi 15546 climrlim2 15583 climrecl 15619 climge0 15620 iseralt 15721 climfsum 15856 structex 17187 issubc 17880 pmtrfv 19470 dprdval 20023 frgpcyg 21592 lindff 21835 lindfind 21836 f1lindf 21842 lindfmm 21847 lsslindf 21850 lbslcic 21861 psrbaglesupp 21942 hauspwdom 23509 refbas 23518 refssex 23519 reftr 23522 refun0 23523 ovoliunnul 25542 dvle 26046 cyclnspth 29821 hlimi 31207 gsumhashmul 33064 extdgval 33705 usgrgt2cycl 35135 brsset 35890 brbigcup 35899 elfix2 35905 brcolinear2 36059 isfne 36340 refssfne 36359 bj-epelg 37069 bj-ideqb 37160 bj-opelidb1ALT 37167 ovoliunnfl 37669 voliunnfl 37671 volsupnfl 37672 brabg2 37724 heiborlem4 37821 isrngo 37904 isdivrngo 37957 brssr 38502 issetssr 38504 fphpd 42827 ctbnfien 42829 sdomne0 43426 climd 45687 climuzlem 45758 rlimdmafv 47189 rlimdmafv2 47270 fuco112 49024 fuco111 49025 fuco21 49031 fucoid 49043 |
| Copyright terms: Public domain | W3C validator |