brel - Metamath Proof Explorer

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

Theorem brel 5037

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

Colors of variables: wff setvar class

Syntax hints:

wi 4 $/\$ wa 367

wcel 1823

wss 3461 class class class wbr 4439

cxp 4986

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1623 ax-4 1636 ax-5 1709 ax-6 1752 ax-7 1795 ax-9 1827 ax-10 1842 ax-11 1847 ax-12 1859 ax-13 2004 ax-ext 2432 ax-sep 4560 ax-nul 4568 ax-pr 4676

This theorem depends on definitions: df-bi 185 df-or 368 df-an 369 df-3an 973 df-tru 1401 df-ex 1618 df-nf 1622 df-sb 1745 df-clab 2440 df-cleq 2446 df-clel 2449 df-nfc 2604 df-ne 2651 df-ral 2809 df-rex 2810 df-rab 2813 df-v 3108 df-dif 3464 df-un 3466 df-in 3468 df-ss 3475 df-nul 3784 df-if 3930 df-sn 4017 df-pr 4019 df-op 4023 df-br 4440 df-opab 4498 df-xp 4994

This theorem is referenced by: brab2a 5038 brab2ga 5064 soirri 5381 sotri 5382 sotri2 5384 sotri3 5385 ndmovord 6438 ndmovordi 6439 swoer 7331 brecop2 7397 ecopovsym 7405 ecopovtrn 7406 hartogslem1 7959 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 11356 dflt2 11357 dvdszrcl 14075 letsr 16056 hmphtop 20445 vcex 25671 brtxp2 29759 brpprod3a 29764

W3C validator