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 5926

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

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

**Proof of Theorem releldm**
Step	Hyp	Ref	Expression
1		brrelex1 5704	. 2 ⊢ ((Rel 𝑅 ∧ 𝐴𝑅𝐵) → 𝐴 ∈ V)
2		brrelex2 5705	. 2 ⊢ ((Rel 𝑅 ∧ 𝐴𝑅𝐵) → 𝐵 ∈ V)
3		simpr 490	. 2 ⊢ ((Rel 𝑅 ∧ 𝐴𝑅𝐵) → 𝐴𝑅𝐵)
4		breldmg 5891	. 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 3451 class class class wbr 5103 dom cdm 5651 Rel wrel 5656

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 2733 ax-sep 5249 ax-pr 5391

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 2740 df-cleq 2753 df-clel 2836 df-ral 3078 df-rex 3088 df-rab 3414 df-v 3453 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 5657 df-rel 5658 df-dm 5661

This theorem is used by: releldmb 5928 releldmi 5930 sofld 6179 funeu 6565 fnbr 6647 funbrfv2b 6942 funfvbrb 7050 ercl 8729 inviso1 17941 setciso 18266 rngciso 20890 ringciso 20924 lmle 25622 dvidlem 26235 dvmulbr 26259 dvcobr 26266 ulmcau 26722 ulmdvlem3 26729 metideq 34525 heibor1lem 38743 rrncmslem 38766 eqvrelcl 39628 ntrclsiex 45052 ntrneiiex 45075 binomcxplemnn0 45332 binomcxplemnotnn0 45339 sumnnodd 46641 climlimsup 46769 climlimsupcex 46778 climliminflimsupd 46810 liminflimsupclim 46816 dmclimxlim 46860 xlimclimdm 46863 xlimresdm 46868 ioodvbdlimc1lem2 46941 ioodvbdlimc2lem 46943 funbrafv 48227 funbrafv2b 48228 rngcisoALTV 49373 ringcisoALTV 49407 isinito3 50607

W3C validator