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 5936

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

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

**Proof of Theorem releldm**
Step	Hyp	Ref	Expression
1		brrelex1 5716	. 2 ⊢ ((Rel 𝑅 ∧ 𝐴𝑅𝐵) → 𝐴 ∈ V)
2		brrelex2 5717	. 2 ⊢ ((Rel 𝑅 ∧ 𝐴𝑅𝐵) → 𝐵 ∈ V)
3		simpr 490	. 2 ⊢ ((Rel 𝑅 ∧ 𝐴𝑅𝐵) → 𝐴𝑅𝐵)
4		breldmg 5901	. 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 3457 class class class wbr 5111 dom cdm 5663 Rel wrel 5668

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 2148 ax-9 2156 ax-ext 2737 ax-sep 5259 ax-pr 5406

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 2744 df-cleq 2757 df-clel 2840 df-ral 3082 df-rex 3092 df-rab 3419 df-v 3459 df-dif 3909 df-un 3911 df-in 3913 df-ss 3923 df-nul 4287 df-if 4490 df-sn 4592 df-pr 4594 df-op 4598 df-br 5112 df-opab 5176 df-xp 5669 df-rel 5670 df-dm 5673

This theorem is used by: releldmb 5938 releldmi 5940 sofld 6187 funeu 6565 fnbr 6647 funbrfv2b 6942 funfvbrb 7050 ercl 8712 inviso1 17845 setciso 18170 rngciso 20787 ringciso 20821 lmle 25511 dvidlem 26125 dvmulbr 26149 dvcobr 26156 ulmcau 26609 ulmdvlem3 26616 metideq 34347 heibor1lem 38518 rrncmslem 38541 eqvrelcl 39403 ntrclsiex 44837 ntrneiiex 44860 binomcxplemnn0 45117 binomcxplemnotnn0 45124 sumnnodd 46404 climlimsup 46532 climlimsupcex 46541 climliminflimsupd 46573 liminflimsupclim 46579 dmclimxlim 46623 xlimclimdm 46626 xlimresdm 46631 ioodvbdlimc1lem2 46704 ioodvbdlimc2lem 46706 funbrafv 47953 funbrafv2b 47954 rngcisoALTV 49099 ringcisoALTV 49133 isinito3 50335

W3C validator