![]() |
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 5456 | . 2 ⊢ ((Rel 𝑅 ∧ 𝐴𝑅𝐵) → 𝐵 ∈ V) | |
3 | 1, 2 | mpan 677 | 1 ⊢ (𝐴𝑅𝐵 → 𝐵 ∈ V) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2050 Vcvv 3415 class class class wbr 4929 Rel wrel 5412 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1758 ax-4 1772 ax-5 1869 ax-6 1928 ax-7 1965 ax-8 2052 ax-9 2059 ax-10 2079 ax-11 2093 ax-12 2106 ax-ext 2750 ax-sep 5060 ax-nul 5067 ax-pr 5186 |
This theorem depends on definitions: df-bi 199 df-an 388 df-or 834 df-3an 1070 df-tru 1510 df-ex 1743 df-nf 1747 df-sb 2016 df-clab 2759 df-cleq 2771 df-clel 2846 df-nfc 2918 df-ral 3093 df-rex 3094 df-rab 3097 df-v 3417 df-dif 3832 df-un 3834 df-in 3836 df-ss 3843 df-nul 4179 df-if 4351 df-sn 4442 df-pr 4444 df-op 4448 df-br 4930 df-opab 4992 df-xp 5413 df-rel 5414 |
This theorem is referenced by: vtoclr 5465 brfvopabrbr 6592 brdomi 8317 domdifsn 8396 undom 8401 xpdom2 8408 xpdom1g 8410 domunsncan 8413 enfixsn 8422 fodomr 8464 pwdom 8465 domssex 8474 xpen 8476 mapdom1 8478 mapdom2 8484 pwen 8486 sucdom2 8509 unxpdom 8520 unxpdom2 8521 sucxpdom 8522 isfinite2 8571 infn0 8575 fin2inf 8576 suppeqfsuppbi 8642 fsuppsssupp 8644 fsuppunbi 8649 funsnfsupp 8652 mapfien2 8667 wemapso2 8812 card2on 8813 elharval 8822 harword 8824 brwdomi 8827 brwdomn0 8828 domwdom 8833 wdomtr 8834 wdompwdom 8837 canthwdom 8838 brwdom3i 8842 unwdomg 8843 xpwdomg 8844 unxpwdom 8848 infdifsn 8914 infdiffi 8915 isnum2 9168 wdomfil 9281 djuen 9393 djuenun 9394 djudom2 9407 djuxpdom 9409 djuinf 9412 infdju1 9413 pwdjuidm 9415 djulepw 9416 infdjuabs 9426 infdif 9429 pwdjudom 9436 infpss 9437 infmap2 9438 fictb 9465 infpssALT 9533 enfin2i 9541 fin34 9610 fodomb 9746 wdomac 9747 iundom2g 9760 iundom 9762 sdomsdomcard 9780 infxpidm 9782 engch 9848 fpwwe2lem3 9853 canthp1lem1 9872 canthp1lem2 9873 canthp1 9874 pwfseq 9884 pwxpndom2 9885 pwxpndom 9886 pwdjundom 9887 hargch 9893 gchaclem 9898 hasheni 13523 hashdomi 13554 brfi1indALT 13669 clim 14712 rlim 14713 ntrivcvgn0 15114 ssc1 16949 ssc2 16950 ssctr 16953 frgpnabl 18751 dprddomprc 18872 dprdval 18875 dprdgrp 18877 dprdf 18878 dprdssv 18888 subgdmdprd 18906 dprd2da 18914 1stcrestlem 21764 hauspwdom 21813 isref 21821 ufilen 22242 dvle 24307 locfinref 30755 isfne4 33215 fnetr 33226 topfneec 33230 fnessref 33232 refssfne 33233 bj-elep 33875 phpreu 34323 climf 41340 climf2 41384 |
Copyright terms: Public domain | W3C validator |