qliftel

Description: Elementhood in the relation F . (Contributed by Mario Carneiro, 23-Dec-2016) (Revised by AV, 3-Aug-2024)

	Ref	Expression
Hypotheses	qlift.1	$⊢ F = ran (x \in X ⟼ ⟨[x] R, A⟩)$
	qlift.2	$⊢ (φ \land x \in X) \to A \in Y$
	qlift.3	$⊢ φ \to R Er X$
	qlift.4	$⊢ φ \to X \in V$
Assertion	qliftel	$⊢ φ \to ([C] R F D \leftrightarrow \exists x \in X (C R x \land D = A))$

Step	Hyp	Ref	Expression
1		qlift.1	$⊢ F = ran (x \in X ⟼ ⟨[x] R, A⟩)$
2		qlift.2	$⊢ (φ \land x \in X) \to A \in Y$
3		qlift.3	$⊢ φ \to R Er X$
4		qlift.4	$⊢ φ \to X \in V$
5	1 2 3 4	qliftlem	$⊢ (φ \land x \in X) \to [x] R \in (X / R)$
6	1 5 2	fliftel	$⊢ φ \to ([C] R F D \leftrightarrow \exists x \in X ([C] R = [x] R \land D = A))$
7	3	adantr	$⊢ (φ \land x \in X) \to R Er X$
8		simpr	$⊢ (φ \land x \in X) \to x \in X$
9	7 8	erth2	$⊢ (φ \land x \in X) \to (C R x \leftrightarrow [C] R = [x] R)$
10	9	anbi1d	$⊢ (φ \land x \in X) \to ((C R x \land D = A) \leftrightarrow ([C] R = [x] R \land D = A))$
11	10	rexbidva	$⊢ φ \to (\exists x \in X (C R x \land D = A) \leftrightarrow \exists x \in X ([C] R = [x] R \land D = A))$
12	6 11	bitr4d	$⊢ φ \to ([C] R F D \leftrightarrow \exists x \in X (C R x \land D = A))$

Metamath Proof Explorer