![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > brrelexi | 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 |
---|---|
brrelexi | ⊢ (𝐴𝑅𝐵 → 𝐴 ∈ V) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | brrelexi.1 | . 2 ⊢ Rel 𝑅 | |
2 | brrelex 5190 | . 2 ⊢ ((Rel 𝑅 ∧ 𝐴𝑅𝐵) → 𝐴 ∈ V) | |
3 | 1, 2 | mpan 706 | 1 ⊢ (𝐴𝑅𝐵 → 𝐴 ∈ V) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2030 Vcvv 3231 class class class wbr 4685 Rel wrel 5148 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1762 ax-4 1777 ax-5 1879 ax-6 1945 ax-7 1981 ax-9 2039 ax-10 2059 ax-11 2074 ax-12 2087 ax-13 2282 ax-ext 2631 ax-sep 4814 ax-nul 4822 ax-pr 4936 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-3an 1056 df-tru 1526 df-ex 1745 df-nf 1750 df-sb 1938 df-clab 2638 df-cleq 2644 df-clel 2647 df-nfc 2782 df-ral 2946 df-rex 2947 df-rab 2950 df-v 3233 df-dif 3610 df-un 3612 df-in 3614 df-ss 3621 df-nul 3949 df-if 4120 df-sn 4211 df-pr 4213 df-op 4217 df-br 4686 df-opab 4746 df-xp 5149 df-rel 5150 |
This theorem is referenced by: nprrel 5195 vtoclr 5198 opeliunxp2 5293 ideqg 5306 issetid 5309 dffv2 6310 brfvopabrbr 6318 brrpssg 6981 opeliunxp2f 7381 brtpos2 7403 brdomg 8007 isfi 8021 en1uniel 8069 domdifsn 8084 undom 8089 xpdom2 8096 xpdom1g 8098 sbth 8121 dom0 8129 sdom0 8133 sdomirr 8138 sdomdif 8149 fodomr 8152 pwdom 8153 xpen 8164 pwen 8174 php3 8187 sucdom2 8197 sdom1 8201 fineqv 8216 f1finf1o 8228 infsdomnn 8262 relprcnfsupp 8319 fsuppimp 8322 fsuppunbi 8337 mapfien2 8355 harword 8511 brwdom 8513 domwdom 8520 brwdom3i 8529 unwdomg 8530 xpwdomg 8531 infdifsn 8592 ac10ct 8895 inffien 8924 iunfictbso 8975 cdaen 9033 cdadom1 9046 cdafi 9050 cdainflem 9051 cdalepw 9056 unctb 9065 infcdaabs 9066 infunabs 9067 infmap2 9078 cfslb2n 9128 fin4i 9158 isfin5 9159 isfin6 9160 fin4en1 9169 isfin4-3 9175 isfin32i 9225 fin45 9252 fin56 9253 fin67 9255 hsmexlem1 9286 hsmexlem3 9288 axcc3 9298 ttukeylem1 9369 brdom3 9388 iundom2g 9400 iundom 9402 iunctb 9434 gchi 9484 engch 9488 gchdomtri 9489 fpwwe2lem6 9495 fpwwe2lem7 9496 fpwwe2lem9 9498 gchpwdom 9530 prcdnq 9853 reexALT 11864 hasheni 13176 hashdomi 13207 brfi1indALT 13320 climcl 14274 climi 14285 climrlim2 14322 climrecl 14358 climge0 14359 iseralt 14459 climfsum 14596 structex 15915 issubc 16542 pmtrfv 17918 dprdval 18448 frgpcyg 19970 lindff 20202 lindfind 20203 f1lindf 20209 lindfmm 20214 lsslindf 20217 lbslcic 20228 1stcrestlem 21303 2ndcdisj2 21308 dis2ndc 21311 hauspwdom 21352 refbas 21361 refssex 21362 reftr 21365 refun0 21366 ovoliunnul 23321 uniiccdif 23392 dvle 23815 subgrv 26207 cyclnspth 26751 hlimi 28173 brsset 32121 brbigcup 32130 elfix2 32136 brcolinear2 32290 isfne 32459 refssfne 32478 ovoliunnfl 33581 voliunnfl 33583 volsupnfl 33584 brabg2 33640 heiborlem4 33743 isrngo 33826 isdivrngo 33879 brssr 34391 fphpd 37697 ctbnfien 37699 climd 40222 climuzlem 40293 rlimdmafv 41578 linindsv 42559 |
Copyright terms: Public domain | W3C validator |