Theorem qliftel1

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=\mathrm{ran}\left(x\in X⟼⟨\left[x\right]R,A⟩\right)$$
	qlift.2	$$⊢\left(\phi \wedge x\in X\right)\to A\in Y$$
	qlift.3	$$⊢\phi \to R\mathrm{Er}X$$
	qlift.4	$$⊢\phi \to X\in V$$
Assertion	qliftel1	$$⊢\left(\phi \wedge x\in X\right)\to \left[x\right]RFA$$

Proof

Step	Hyp	Ref	Expression
1		qlift.1	$$⊢F=\mathrm{ran}\left(x\in X⟼⟨\left[x\right]R,A⟩\right)$$
2		qlift.2	$$⊢\left(\phi \wedge x\in X\right)\to A\in Y$$
3		qlift.3	$$⊢\phi \to R\mathrm{Er}X$$
4		qlift.4	$$⊢\phi \to X\in V$$
5	1 2 3 4	qliftlem	$$⊢\left(\phi \wedge x\in X\right)\to \left[x\right]R\in \left(X/R\right)$$
6	1 5 2	fliftel1	$$⊢\left(\phi \wedge x\in X\right)\to \left[x\right]RFA$$