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 5642 | . 2 ⊢ ((Rel 𝑅 ∧ 𝐴𝑅𝐵) → 𝐵 ∈ V) | |
3 | 1, 2 | mpan 687 | 1 ⊢ (𝐴𝑅𝐵 → 𝐵 ∈ V) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2107 Vcvv 3433 class class class wbr 5075 Rel wrel 5595 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-ext 2710 ax-sep 5224 ax-nul 5231 ax-pr 5353 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 845 df-3an 1088 df-tru 1542 df-fal 1552 df-ex 1783 df-sb 2069 df-clab 2717 df-cleq 2731 df-clel 2817 df-ral 3070 df-rex 3071 df-rab 3074 df-v 3435 df-dif 3891 df-un 3893 df-in 3895 df-ss 3905 df-nul 4258 df-if 4461 df-sn 4563 df-pr 4565 df-op 4569 df-br 5076 df-opab 5138 df-xp 5596 df-rel 5597 |
This theorem is referenced by: vtoclr 5651 brfvopabrbr 6881 brdomiOLD 8758 domdifsn 8850 undom 8855 undomOLD 8856 xpdom2 8863 xpdom1g 8865 domunsncan 8868 enfixsn 8877 sucdom2OLD 8878 fodomr 8924 pwdom 8925 domssex 8934 xpen 8936 mapdom1 8938 mapdom2 8944 pwen 8946 domtrfil 8987 sucdom2 8998 unxpdom 9039 unxpdom2 9040 sucxpdom 9041 isfinite2 9081 infn0 9085 fin2inf 9086 suppeqfsuppbi 9151 fsuppsssupp 9153 fsuppunbi 9158 funsnfsupp 9161 mapfien2 9177 wemapso2 9321 card2on 9322 elharval 9329 harword 9331 brwdomi 9336 brwdomn0 9337 domwdom 9342 wdomtr 9343 wdompwdom 9346 canthwdom 9347 brwdom3i 9351 unwdomg 9352 xpwdomg 9353 unxpwdom 9357 infdifsn 9424 infdiffi 9425 isnum2 9712 wdomfil 9826 djuen 9934 djuenun 9935 djudom2 9948 djuxpdom 9950 djuinf 9953 infdju1 9954 pwdjuidm 9956 djulepw 9957 infdjuabs 9971 infdif 9974 pwdjudom 9981 infpss 9982 infmap2 9983 fictb 10010 infpssALT 10078 enfin2i 10086 fin34 10155 fodomb 10291 wdomac 10292 iundom2g 10305 iundom 10307 sdomsdomcard 10325 infxpidm 10327 engch 10393 fpwwe2lem3 10398 canthp1lem1 10417 canthp1lem2 10418 canthp1 10419 pwfseq 10429 pwxpndom2 10430 pwxpndom 10431 pwdjundom 10432 hargch 10438 gchaclem 10443 hasheni 14071 hashdomi 14104 clim 15212 rlim 15213 ntrivcvgn0 15619 ssc1 17542 ssc2 17543 ssctr 17546 frgpnabl 19485 dprddomprc 19612 dprdval 19615 dprdgrp 19617 dprdf 19618 dprdssv 19628 subgdmdprd 19646 dprd2da 19654 1stcrestlem 22612 hauspwdom 22661 isref 22669 ufilen 23090 dvle 25180 locfinref 31800 isfne4 34538 fnetr 34549 topfneec 34553 fnessref 34555 refssfne 34556 bj-epelb 35249 bj-idreseq 35342 phpreu 35770 climf 43170 climf2 43214 |
Copyright terms: Public domain | W3C validator |