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 5168

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 4697	. 2
3		brxp 5147	. 2 $/\$
4	2, 3	sylib 208	1 $/\$

Colors of variables: wff setvar class

Syntax hints:

wi 4 $/\$ wa 384

wcel 1990

wss 3574 class class class wbr 4653

cxp 5112

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

This theorem is referenced by: brab2a 5194 soirri 5522 sotri 5523 sotri2 5525 sotri3 5526 ndmovord 6824 ndmovordi 6825 swoer 7772 brecop2 7841 ecopovsym 7849 ecopovtrn 7850 hartogslem1 8447 nlt1pi 9728 indpi 9729 nqerf 9752 ordpipq 9764 lterpq 9792 ltexnq 9797 ltbtwnnq 9800 ltrnq 9801 prnmadd 9819 genpcd 9828 nqpr 9836 1idpr 9851 ltexprlem4 9861 ltexpri 9865 ltaprlem 9866 prlem936 9869 reclem2pr 9870 reclem3pr 9871 reclem4pr 9872 suplem1pr 9874 suplem2pr 9875 supexpr 9876 recexsrlem 9924 addgt0sr 9925 mulgt0sr 9926 mappsrpr 9929 map2psrpr 9931 supsrlem 9932 supsr 9933 ltresr 9961 dfle2 11980 dflt2 11981 dvdszrcl 14988 letsr 17227 hmphtop 21581 vcex 27433 brtxp2 31988 brpprod3a 31993

W3C validator