Metamath Proof Explorer

Theorem brelrng

Description: The second argument of a binary relation belongs to its range. (Contributed by NM, 29-Jun-2008)

Ref Expression
Assertion brelrng ⊢ A ∈ F ∧ B ∈ G ∧ A C B → B ∈ ran ⁡ C

Proof

Step Hyp Ref Expression
1 brcnvg ⊢ B ∈ G ∧ A ∈ F → B C -1 A ↔ A C B
2 1 ancoms ⊢ A ∈ F ∧ B ∈ G → B C -1 A ↔ A C B
3 2 biimp3ar ⊢ A ∈ F ∧ B ∈ G ∧ A C B → B C -1 A
4 breldmg ⊢ B ∈ G ∧ A ∈ F ∧ B C -1 A → B ∈ dom ⁡ C -1
5 4 3com12 ⊢ A ∈ F ∧ B ∈ G ∧ B C -1 A → B ∈ dom ⁡ C -1
6 3 5 syld3an3 ⊢ A ∈ F ∧ B ∈ G ∧ A C B → B ∈ dom ⁡ C -1
7 df-rn ⊢ ran ⁡ C = dom ⁡ C -1
8 6 7 eleqtrrdi ⊢ A ∈ F ∧ B ∈ G ∧ A C B → B ∈ ran ⁡ C