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 5943

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

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

**Proof of Theorem releldm**
Step	Hyp	Ref	Expression
1		brrelex1 5729	. 2 ⊢ ((Rel 𝑅 ∧ 𝐴𝑅𝐵) → 𝐴 ∈ V)
2		brrelex2 5730	. 2 ⊢ ((Rel 𝑅 ∧ 𝐴𝑅𝐵) → 𝐵 ∈ V)
3		simpr 484	. 2 ⊢ ((Rel 𝑅 ∧ 𝐴𝑅𝐵) → 𝐴𝑅𝐵)
4		breldmg 5909	. 2 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝐴𝑅𝐵) → 𝐴 ∈ dom 𝑅)
5	1, 2, 3, 4	syl3anc 1370	1 ⊢ ((Rel 𝑅 ∧ 𝐴𝑅𝐵) → 𝐴 ∈ dom 𝑅)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 395 ∈ wcel 2105 Vcvv 3473 class class class wbr 5148 dom cdm 5676 Rel wrel 5681

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1912 ax-6 1970 ax-7 2010 ax-8 2107 ax-9 2115 ax-ext 2702 ax-sep 5299 ax-nul 5306 ax-pr 5427

This theorem depends on definitions: df-bi 206 df-an 396 df-or 845 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1781 df-sb 2067 df-clab 2709 df-cleq 2723 df-clel 2809 df-ral 3061 df-rex 3070 df-rab 3432 df-v 3475 df-dif 3951 df-un 3953 df-in 3955 df-ss 3965 df-nul 4323 df-if 4529 df-sn 4629 df-pr 4631 df-op 4635 df-br 5149 df-opab 5211 df-xp 5682 df-rel 5683 df-dm 5686

This theorem is referenced by: releldmb 5945 releldmi 5947 sofld 6186 funeu 6573 fnbr 6657 funbrfv2b 6949 funfvbrb 7052 ercl 8720 inviso1 17720 setciso 18051 rngciso 20530 ringciso 20564 lmle 25148 dvidlem 25763 dvmulbr 25788 dvmulbrOLD 25789 dvcobr 25796 dvcobrOLD 25797 ulmcau 26245 ulmdvlem3 26252 metideq 33336 heibor1lem 37140 rrncmslem 37163 eqvrelcl 37945 ntrclsiex 43266 ntrneiiex 43289 binomcxplemnn0 43570 binomcxplemnotnn0 43577 sumnnodd 44804 climlimsup 44934 climlimsupcex 44943 climliminflimsupd 44975 liminflimsupclim 44981 dmclimxlim 45025 xlimclimdm 45028 xlimresdm 45033 ioodvbdlimc1lem2 45106 ioodvbdlimc2lem 45108 funbrafv 46324 funbrafv2b 46325 rngcisoALTV 47113 ringcisoALTV 47147

W3C validator