eltail

Description: An element of a tail. (Contributed by Jeff Hankins, 25-Nov-2009) (Revised by Mario Carneiro, 24-Nov-2013)

		Ref	Expression
	Hypothesis	tailfval.1	$⊢ X = dom D$
	Assertion	eltail	$⊢ (D \in DirRel \land A \in X \land B \in C) \to (B \in tail (D) (A) \leftrightarrow A D B)$

Step	Hyp	Ref	Expression
1		tailfval.1	$⊢ X = dom D$
2	1	tailval	$⊢ (D \in DirRel \land A \in X) \to tail (D) (A) = D [\{A\}]$
3	2	eleq2d	$⊢ (D \in DirRel \land A \in X) \to (B \in tail (D) (A) \leftrightarrow B \in D [\{A\}])$
4	3	3adant3	$⊢ (D \in DirRel \land A \in X \land B \in C) \to (B \in tail (D) (A) \leftrightarrow B \in D [\{A\}])$
5		elimasng	$⊢ (A \in X \land B \in C) \to (B \in D [\{A\}] \leftrightarrow ⟨A, B⟩ \in D)$
6		df-br	$⊢ A D B \leftrightarrow ⟨A, B⟩ \in D$
7	5 6	bitr4di	$⊢ (A \in X \land B \in C) \to (B \in D [\{A\}] \leftrightarrow A D B)$
8	7	3adant1	$⊢ (D \in DirRel \land A \in X \land B \in C) \to (B \in D [\{A\}] \leftrightarrow A D B)$
9	4 8	bitrd	$⊢ (D \in DirRel \land A \in X \land B \in C) \to (B \in tail (D) (A) \leftrightarrow A D B)$

Metamath Proof Explorer