fliftel

Description: Elementhood in the relation F . (Contributed by Mario Carneiro, 23-Dec-2016)

	Ref	Expression
Hypotheses	flift.1	$⊢ F = ran (x \in X ⟼ ⟨A, B⟩)$
	flift.2	$⊢ (φ \land x \in X) \to A \in R$
	flift.3	$⊢ (φ \land x \in X) \to B \in S$
Assertion	fliftel	$⊢ φ \to (C F D \leftrightarrow \exists x \in X (C = A \land D = B))$

Step	Hyp	Ref	Expression
1		flift.1	$⊢ F = ran (x \in X ⟼ ⟨A, B⟩)$
2		flift.2	$⊢ (φ \land x \in X) \to A \in R$
3		flift.3	$⊢ (φ \land x \in X) \to B \in S$
4		df-br	$⊢ C F D \leftrightarrow ⟨C, D⟩ \in F$
5	1	eleq2i	$⊢ ⟨C, D⟩ \in F \leftrightarrow ⟨C, D⟩ \in ran (x \in X ⟼ ⟨A, B⟩)$
6		eqid	$⊢ (x \in X ⟼ ⟨A, B⟩) = (x \in X ⟼ ⟨A, B⟩)$
7		opex	$⊢ ⟨A, B⟩ \in V$
8	6 7	elrnmpti	$⊢ ⟨C, D⟩ \in ran (x \in X ⟼ ⟨A, B⟩) \leftrightarrow \exists x \in X ⟨C, D⟩ = ⟨A, B⟩$
9	4 5 8	3bitri	$⊢ C F D \leftrightarrow \exists x \in X ⟨C, D⟩ = ⟨A, B⟩$
10		opthg2	$⊢ (A \in R \land B \in S) \to (⟨C, D⟩ = ⟨A, B⟩ \leftrightarrow (C = A \land D = B))$
11	2 3 10	syl2anc	$⊢ (φ \land x \in X) \to (⟨C, D⟩ = ⟨A, B⟩ \leftrightarrow (C = A \land D = B))$
12	11	rexbidva	$⊢ φ \to (\exists x \in X ⟨C, D⟩ = ⟨A, B⟩ \leftrightarrow \exists x \in X (C = A \land D = B))$
13	9 12	syl5bb	$⊢ φ \to (C F D \leftrightarrow \exists x \in X (C = A \land D = B))$

Metamath Proof Explorer