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 4886

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 4448	. 2
3		brxp 4868	. 2 $/\$
4	2, 3	sylib 200	1 $/\$

Colors of variables: wff setvar class

Syntax hints:

wi 4 $/\$ wa 371

wcel 1889

wss 3406 class class class wbr 4405

cxp 4835

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1671 ax-4 1684 ax-5 1760 ax-6 1807 ax-7 1853 ax-9 1898 ax-10 1917 ax-11 1922 ax-12 1935 ax-13 2093 ax-ext 2433 ax-sep 4528 ax-nul 4537 ax-pr 4642

This theorem depends on definitions: df-bi 189 df-or 372 df-an 373 df-3an 988 df-tru 1449 df-ex 1666 df-nf 1670 df-sb 1800 df-clab 2440 df-cleq 2446 df-clel 2449 df-nfc 2583 df-ne 2626 df-ral 2744 df-rex 2745 df-rab 2748 df-v 3049 df-dif 3409 df-un 3411 df-in 3413 df-ss 3420 df-nul 3734 df-if 3884 df-sn 3971 df-pr 3973 df-op 3977 df-br 4406 df-opab 4465 df-xp 4843

This theorem is referenced by: brab2a 4887 brab2ga 4913 soirri 5229 sotri 5230 sotri2 5232 sotri3 5233 ndmovord 6464 ndmovordi 6465 swoer 7396 brecop2 7462 ecopovsym 7470 ecopovtrn 7471 hartogslem1 8062 nlt1pi 9336 indpi 9337 nqerf 9360 ordpipq 9372 lterpq 9400 ltexnq 9405 ltbtwnnq 9408 ltrnq 9409 prnmadd 9427 genpcd 9436 nqpr 9444 1idpr 9459 ltexprlem4 9469 ltexpri 9473 ltaprlem 9474 prlem936 9477 reclem2pr 9478 reclem3pr 9479 reclem4pr 9480 suplem1pr 9482 suplem2pr 9483 supexpr 9484 recexsrlem 9532 addgt0sr 9533 mulgt0sr 9534 mappsrpr 9537 map2psrpr 9539 supsrlem 9540 supsr 9541 ltresr 9569 dfle2 11453 dflt2 11454 dvdszrcl 14322 letsr 16485 hmphtop 20805 vcex 26211 brtxp2 30660 brpprod3a 30665

W3C validator