![]() |
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 5736 | . 2 ⊢ ((Rel 𝑅 ∧ 𝐴𝑅𝐵) → 𝐵 ∈ V) | |
3 | 1, 2 | mpan 688 | 1 ⊢ (𝐴𝑅𝐵 → 𝐵 ∈ V) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2098 Vcvv 3473 class class class wbr 5152 Rel wrel 5687 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-ext 2699 ax-sep 5303 ax-nul 5310 ax-pr 5433 |
This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-3an 1086 df-tru 1536 df-fal 1546 df-ex 1774 df-sb 2060 df-clab 2706 df-cleq 2720 df-clel 2806 df-ral 3059 df-rex 3068 df-rab 3431 df-v 3475 df-dif 3952 df-un 3954 df-in 3956 df-ss 3966 df-nul 4327 df-if 4533 df-sn 4633 df-pr 4635 df-op 4639 df-br 5153 df-opab 5215 df-xp 5688 df-rel 5689 |
This theorem is referenced by: vtoclr 5745 brfvopabrbr 7007 brdomiOLD 8986 domdifsn 9085 undom 9090 undomOLD 9091 xpdom2 9098 xpdom1g 9100 domunsncan 9103 enfixsn 9112 sucdom2OLD 9113 fodomr 9159 pwdom 9160 domssex 9169 xpen 9171 mapdom1 9173 mapdom2 9179 pwen 9181 domtrfil 9226 sucdom2 9237 0sdom1dom 9269 1sdom2dom 9278 unxpdom 9284 unxpdom2 9285 sucxpdom 9286 isfinite2 9332 infn0ALT 9339 fin2inf 9340 suppeqfsuppbi 9410 fsuppsssupp 9412 fsuppssov1 9415 fsuppunbi 9420 funsnfsupp 9423 mapfien2 9440 wemapso2 9584 card2on 9585 elharval 9592 harword 9594 brwdomi 9599 brwdomn0 9600 domwdom 9605 wdomtr 9606 wdompwdom 9609 canthwdom 9610 brwdom3i 9614 unwdomg 9615 xpwdomg 9616 unxpwdom 9620 infdifsn 9688 infdiffi 9689 isnum2 9976 wdomfil 10092 djuen 10200 djuenun 10201 djudom2 10214 djuxpdom 10216 djuinf 10219 infdju1 10220 pwdjuidm 10222 djulepw 10223 infdjuabs 10237 infdif 10240 pwdjudom 10247 infpss 10248 infmap2 10249 fictb 10276 infpssALT 10344 enfin2i 10352 fin34 10421 fodomb 10557 wdomac 10558 iundom2g 10571 iundom 10573 sdomsdomcard 10591 infxpidm 10593 engch 10659 fpwwe2lem3 10664 canthp1lem1 10683 canthp1lem2 10684 canthp1 10685 pwfseq 10695 pwxpndom2 10696 pwxpndom 10697 pwdjundom 10698 hargch 10704 gchaclem 10709 hasheni 14347 hashdomi 14379 clim 15478 rlim 15479 ntrivcvgn0 15884 ssc1 17811 ssc2 17812 ssctr 17815 frgpnabl 19837 dprddomprc 19964 dprdval 19967 dprdgrp 19969 dprdf 19970 dprdssv 19980 subgdmdprd 19998 dprd2da 20006 1stcrestlem 23376 hauspwdom 23425 isref 23433 ufilen 23854 dvle 25960 ellpi 33110 locfinref 33475 isfne4 35857 fnetr 35868 topfneec 35872 fnessref 35874 refssfne 35875 bj-epelb 36581 bj-idreseq 36674 phpreu 37110 sdomne0 42874 sdomne0d 42875 rn1st 44679 climf 45039 climf2 45083 |
Copyright terms: Public domain | W3C validator |