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 5928

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

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

**Proof of Theorem releldm**
Step	Hyp	Ref	Expression
1		brrelex1 5708	. 2 ⊢ ((Rel 𝑅 ∧ 𝐴𝑅𝐵) → 𝐴 ∈ V)
2		brrelex2 5709	. 2 ⊢ ((Rel 𝑅 ∧ 𝐴𝑅𝐵) → 𝐵 ∈ V)
3		simpr 490	. 2 ⊢ ((Rel 𝑅 ∧ 𝐴𝑅𝐵) → 𝐴𝑅𝐵)
4		breldmg 5893	. 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 2145 Vcvv 3450 class class class wbr 5103 dom cdm 5655 Rel wrel 5660

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2147 ax-9 2155 ax-ext 2732 ax-sep 5251 ax-pr 5398

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-sb 2100 df-clab 2739 df-cleq 2752 df-clel 2835 df-ral 3077 df-rex 3087 df-rab 3413 df-v 3452 df-dif 3902 df-un 3904 df-in 3906 df-ss 3916 df-nul 4280 df-if 4483 df-sn 4585 df-pr 4587 df-op 4591 df-br 5104 df-opab 5168 df-xp 5661 df-rel 5662 df-dm 5665

This theorem is used by: releldmb 5930 releldmi 5932 sofld 6180 funeu 6559 fnbr 6641 funbrfv2b 6936 funfvbrb 7044 ercl 8709 inviso1 17856 setciso 18181 rngciso 20801 ringciso 20835 lmle 25530 dvidlem 26143 dvmulbr 26167 dvcobr 26174 ulmcau 26632 ulmdvlem3 26639 metideq 34404 heibor1lem 38560 rrncmslem 38583 eqvrelcl 39445 ntrclsiex 44894 ntrneiiex 44917 binomcxplemnn0 45174 binomcxplemnotnn0 45181 sumnnodd 46461 climlimsup 46589 climlimsupcex 46598 climliminflimsupd 46630 liminflimsupclim 46636 dmclimxlim 46680 xlimclimdm 46683 xlimresdm 46688 ioodvbdlimc1lem2 46761 ioodvbdlimc2lem 46763 funbrafv 48047 funbrafv2b 48048 rngcisoALTV 49193 ringcisoALTV 49227 isinito3 50427

W3C validator