releldm - Metamath Proof Explorer

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

Theorem releldm 5930

Description: The first argument of a binary relation belongs to its domain. Note that 𝐴𝑅𝐵 does not imply Rel 𝑅: see for example nrelv 5781 and brv 5444. (Contributed by NM, 2-Jul-2008.)

**Assertion**
Ref	Expression
releldm	⊢ ((Rel 𝑅 ∧ 𝐴𝑅𝐵) → 𝐴 ∈ dom 𝑅)

**Proof of Theorem releldm**
Step	Hyp	Ref	Expression
1		brrelex1 5707	. 2 ⊢ ((Rel 𝑅 ∧ 𝐴𝑅𝐵) → 𝐴 ∈ V)
2		brrelex2 5708	. 2 ⊢ ((Rel 𝑅 ∧ 𝐴𝑅𝐵) → 𝐵 ∈ V)
3		simpr 490	. 2 ⊢ ((Rel 𝑅 ∧ 𝐴𝑅𝐵) → 𝐴𝑅𝐵)
4		breldmg 5895	. 2 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝐴𝑅𝐵) → 𝐴 ∈ dom 𝑅)
5	1, 2, 3, 4	syl3anc 1398	1 ⊢ ((Rel 𝑅 ∧ 𝐴𝑅𝐵) → 𝐴 ∈ dom 𝑅)

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ∧ wa 401 ∈ wcel 2146 Vcvv 3453 class class class wbr 5105 dom cdm 5654 Rel wrel 5659

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1827 ax-4 1841 ax-5 1944 ax-6 2001 ax-7 2042 ax-8 2148 ax-9 2156 ax-ext 2735 ax-sep 5251 ax-pr 5394

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3an 1105 df-tru 1572 df-fal 1582 df-ex 1812 df-sb 2101 df-clab 2742 df-cleq 2755 df-clel 2838 df-ral 3080 df-rex 3090 df-rab 3416 df-v 3455 df-ss 3900 df-dif 4049 df-in 4093 df-un 4153 df-nul 4281 df-if 4485 df-sn 4588 df-pr 4590 df-op 4838 df-br 5106 df-opab 5170 df-xp 5660 df-rel 5661 df-dm 5664

This theorem is used by: releldmb 5932 releldmi 5934 sofld 6184 funeu 6573 fnbr 6655 funbrfv2b 6950 funfvbrb 7058 ercl 8740 inviso1 17953 setciso 18278 rngciso 20902 ringciso 20936 lmle 25634 dvidlem 26247 dvmulbr 26271 dvcobr 26278 ulmcau 26734 ulmdvlem3 26741 metideq 34578 heibor1lem 38883 rrncmslem 38906 eqvrelcl 39768 ntrclsiex 45193 ntrneiiex 45216 binomcxplemnn0 45473 binomcxplemnotnn0 45480 sumnnodd 46781 climlimsup 46909 climlimsupcex 46918 climliminflimsupd 46950 liminflimsupclim 46956 dmclimxlim 47000 xlimclimdm 47003 xlimresdm 47008 ioodvbdlimc1lem2 47081 ioodvbdlimc2lem 47083 funbrafv 48367 funbrafv2b 48368 rngcisoALTV 49513 ringcisoALTV 49547 isinito3 50774

W3C validator