brel - Metamath Proof Explorer

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

Theorem brel 5040

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 4482	. 2
3		brxp 5022	. 2 $/\$
4	2, 3	sylib 196	1 $/\$

Colors of variables: wff setvar class

Syntax hints:

wi 4 $/\$ wa 369

wcel 1762

wss 3469 class class class wbr 4440

cxp 4990

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1596 ax-4 1607 ax-5 1675 ax-6 1714 ax-7 1734 ax-9 1766 ax-10 1781 ax-11 1786 ax-12 1798 ax-13 1961 ax-ext 2438 ax-sep 4561 ax-nul 4569 ax-pr 4679

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3an 970 df-tru 1377 df-ex 1592 df-nf 1595 df-sb 1707 df-clab 2446 df-cleq 2452 df-clel 2455 df-nfc 2610 df-ne 2657 df-ral 2812 df-rex 2813 df-rab 2816 df-v 3108 df-dif 3472 df-un 3474 df-in 3476 df-ss 3483 df-nul 3779 df-if 3933 df-sn 4021 df-pr 4023 df-op 4027 df-br 4441 df-opab 4499 df-xp 4998

This theorem is referenced by: brab2a 5041 brab2ga 5066 soirri 5384 sotri 5385 sotri2 5387 sotri3 5388 soirriOLD 5389 sotriOLD 5390 ndmovord 6440 ndmovordi 6441 swoer 7329 brecop2 7395 ecopovsym 7403 ecopovtrn 7404 hartogslem1 7956 nlt1pi 9273 indpi 9274 nqerf 9297 ordpipq 9309 lterpq 9337 ltexnq 9342 ltbtwnnq 9345 ltrnq 9346 prnmadd 9364 genpcd 9373 nqpr 9381 1idpr 9396 ltexprlem4 9406 ltexpri 9410 ltaprlem 9411 prlem936 9414 reclem2pr 9415 reclem3pr 9416 reclem4pr 9417 suplem1pr 9419 suplem2pr 9420 supexpr 9421 recexsrlem 9469 addgt0sr 9470 mulgt0sr 9471 mappsrpr 9474 map2psrpr 9476 supsrlem 9477 supsr 9478 ltresr 9506 dfle2 11342 dflt2 11343 dvdszrcl 13841 letsr 15703 hmphtop 20007 vcex 25135 brtxp2 29094 brpprod3a 29099

W3C validator