brel - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > brel		Structured version Visualization version Unicode version

Theorem brel 4888

Description: Two things in a binary relation belong to the relation's domain. (Contributed by NM, 17-May-1996.) (Revised by Mario Carneiro, 26-Apr-2015.)

**Hypothesis**
Ref	Expression
brel.1

**Assertion**
Ref	Expression
brel	$/\$

**Proof of Theorem brel**
Step	Hyp	Ref	Expression
1		brel.1	. . 3
2	1	ssbri 4438	. 2
3		brxp 4870	. 2 $/\$
4	2, 3	sylib 201	1 $/\$

Colors of variables: wff setvar class

Syntax hints:

wi 4 $/\$ wa 376

wcel 1904

wss 3390 class class class wbr 4395

cxp 4837

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1677 ax-4 1690 ax-5 1766 ax-6 1813 ax-7 1859 ax-9 1913 ax-10 1932 ax-11 1937 ax-12 1950 ax-13 2104 ax-ext 2451 ax-sep 4518 ax-nul 4527 ax-pr 4639

This theorem depends on definitions: df-bi 190 df-or 377 df-an 378 df-3an 1009 df-tru 1455 df-ex 1672 df-nf 1676 df-sb 1806 df-clab 2458 df-cleq 2464 df-clel 2467 df-nfc 2601 df-ne 2643 df-ral 2761 df-rex 2762 df-rab 2765 df-v 3033 df-dif 3393 df-un 3395 df-in 3397 df-ss 3404 df-nul 3723 df-if 3873 df-sn 3960 df-pr 3962 df-op 3966 df-br 4396 df-opab 4455 df-xp 4845

This theorem is referenced by: brab2a 4889 brab2ga 4915 soirri 5232 sotri 5233 sotri2 5235 sotri3 5236 ndmovord 6478 ndmovordi 6479 swoer 7409 brecop2 7475 ecopovsym 7483 ecopovtrn 7484 hartogslem1 8075 nlt1pi 9349 indpi 9350 nqerf 9373 ordpipq 9385 lterpq 9413 ltexnq 9418 ltbtwnnq 9421 ltrnq 9422 prnmadd 9440 genpcd 9449 nqpr 9457 1idpr 9472 ltexprlem4 9482 ltexpri 9486 ltaprlem 9487 prlem936 9490 reclem2pr 9491 reclem3pr 9492 reclem4pr 9493 suplem1pr 9495 suplem2pr 9496 supexpr 9497 recexsrlem 9545 addgt0sr 9546 mulgt0sr 9547 mappsrpr 9550 map2psrpr 9552 supsrlem 9553 supsr 9554 ltresr 9582 dfle2 11469 dflt2 11470 dvdszrcl 14387 letsr 16551 hmphtop 20870 vcex 26280 brtxp2 30719 brpprod3a 30724

W3C validator