| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > brrelex2i | Structured version Visualization version GIF version | ||
| Description: The second argument of a binary relation exists. (An artifact of our ordered pair definition.) (Contributed by Mario Carneiro, 26-Apr-2015.) |
| Ref | Expression |
|---|---|
| brrelexi.1 | ⊢ Rel 𝑅 |
| Ref | Expression |
|---|---|
| brrelex2i | ⊢ (𝐴𝑅𝐵 → 𝐵 ∈ V) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | brrelexi.1 | . 2 ⊢ Rel 𝑅 | |
| 2 | brrelex2 5739 | . 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: vtoclr 5748 brfvopabrbr 7013 brdomiOLD 9000 domdifsn 9094 undom 9099 undomOLD 9100 xpdom2 9107 xpdom1g 9109 domunsncan 9112 enfixsn 9121 sucdom2OLD 9122 fodomr 9168 pwdom 9169 domssex 9178 xpen 9180 mapdom1 9182 mapdom2 9188 pwen 9190 domtrfil 9232 sucdom2 9243 0sdom1dom 9274 1sdom2dom 9283 unxpdom 9289 unxpdom2 9290 sucxpdom 9291 isfinite2 9334 infn0ALT 9341 fin2inf 9342 fodomfir 9368 suppeqfsuppbi 9419 fsuppsssupp 9421 fsuppssov1 9424 fsuppunbi 9429 funsnfsupp 9432 mapfien2 9449 wemapso2 9593 card2on 9594 elharval 9601 harword 9603 brwdomi 9608 brwdomn0 9609 domwdom 9614 wdomtr 9615 wdompwdom 9618 canthwdom 9619 brwdom3i 9623 unwdomg 9624 xpwdomg 9625 unxpwdom 9629 infdifsn 9697 infdiffi 9698 isnum2 9985 wdomfil 10101 djuen 10210 djuenun 10211 djudom2 10224 djuxpdom 10226 djuinf 10229 infdju1 10230 pwdjuidm 10232 djulepw 10233 infdjuabs 10245 infdif 10248 pwdjudom 10255 infpss 10256 infmap2 10257 fictb 10284 infpssALT 10353 enfin2i 10361 fin34 10430 fodomb 10566 wdomac 10567 iundom2g 10580 iundom 10582 sdomsdomcard 10600 infxpidm 10602 engch 10668 fpwwe2lem3 10673 canthp1lem1 10692 canthp1lem2 10693 canthp1 10694 pwfseq 10704 pwxpndom2 10705 pwxpndom 10706 pwdjundom 10707 hargch 10713 gchaclem 10718 hasheni 14387 hashdomi 14419 clim 15530 rlim 15531 ntrivcvgn0 15934 ssc1 17865 ssc2 17866 ssctr 17869 frgpnabl 19893 dprddomprc 20020 dprdval 20023 dprdgrp 20025 dprdf 20026 dprdssv 20036 subgdmdprd 20054 dprd2da 20062 1stcrestlem 23460 hauspwdom 23509 isref 23517 ufilen 23938 dvle 26046 ellpi 33401 locfinref 33840 isfne4 36341 fnetr 36352 topfneec 36356 fnessref 36358 refssfne 36359 bj-epelb 37070 bj-idreseq 37163 phpreu 37611 sdomne0 43426 sdomne0d 43427 rn1st 45280 climf 45637 climf2 45681 fuco21 49031 fucoid 49043 |
| Copyright terms: Public domain | W3C validator |