Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > brrelex2i | Structured version Visualization version Unicode 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 |
Ref | Expression |
---|---|
brrelex2i |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | brrelexi.1 | . 2 | |
2 | brrelex2 5157 | . 2 | |
3 | 1, 2 | mpan 706 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wi 4 wcel 1990 cvv 3200 class class class wbr 4653 wrel 5119 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 ax-sep 4781 ax-nul 4789 ax-pr 4906 |
This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3an 1039 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-ral 2917 df-rex 2918 df-rab 2921 df-v 3202 df-dif 3577 df-un 3579 df-in 3581 df-ss 3588 df-nul 3916 df-if 4087 df-sn 4178 df-pr 4180 df-op 4184 df-br 4654 df-opab 4713 df-xp 5120 df-rel 5121 |
This theorem is referenced by: vtoclr 5164 brfvopabrbr 6279 brdomi 7966 domdifsn 8043 undom 8048 xpdom2 8055 xpdom1g 8057 domunsncan 8060 enfixsn 8069 fodomr 8111 pwdom 8112 domssex 8121 xpen 8123 mapdom1 8125 mapdom2 8131 pwen 8133 sucdom2 8156 unxpdom 8167 unxpdom2 8168 sucxpdom 8169 isfinite2 8218 infn0 8222 fin2inf 8223 fsuppimp 8281 suppeqfsuppbi 8289 fsuppsssupp 8291 fsuppunbi 8296 funsnfsupp 8299 mapfien2 8314 wemapso2 8458 card2on 8459 elharval 8468 harword 8470 brwdomi 8473 brwdomn0 8474 domwdom 8479 wdomtr 8480 wdompwdom 8483 canthwdom 8484 brwdom3i 8488 unwdomg 8489 xpwdomg 8490 unxpwdom 8494 infdifsn 8554 infdiffi 8555 isnum2 8771 wdomfil 8884 cdaen 8995 cdaenun 8996 cdadom1 9008 cdaxpdom 9011 cdainf 9014 infcda1 9015 pwcdaidm 9017 cdalepw 9018 infpss 9039 infmap2 9040 fictb 9067 infpssALT 9135 enfin2i 9143 fin34 9212 fodomb 9348 wdomac 9349 iundom2g 9362 iundom 9364 sdomsdomcard 9382 infxpidm 9384 engch 9450 fpwwe2lem3 9455 canthp1lem1 9474 canthp1lem2 9475 canthp1 9476 pwfseq 9486 pwxpndom2 9487 pwxpndom 9488 pwcdandom 9489 hargch 9495 gchaclem 9500 hasheni 13136 hashdomi 13169 brfi1indALT 13282 brfi1indALTOLD 13288 clim 14225 rlim 14226 ntrivcvgn0 14630 ssc1 16481 ssc2 16482 ssctr 16485 frgpnabl 18278 dprddomprc 18399 dprdval 18402 dprdgrp 18404 dprdf 18405 dprdssv 18415 subgdmdprd 18433 dprd2da 18441 1stcrestlem 21255 hauspwdom 21304 isref 21312 ufilen 21734 dvle 23770 subgrv 26162 locfinref 29908 isfne4 32335 fnetr 32346 topfneec 32350 fnessref 32352 refssfne 32353 phpreu 33393 climf 39854 climf2 39898 linindsv 42234 |
Copyright terms: Public domain | W3C validator |