Theorem fliftel1

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

	Ref	Expression
Hypotheses	flift.1	$$⊢F=\mathrm{ran}\left(x\in X⟼⟨A,B⟩\right)$$
	flift.2	$$⊢\left(\phi \wedge x\in X\right)\to A\in R$$
	flift.3	$$⊢\left(\phi \wedge x\in X\right)\to B\in S$$
Assertion	fliftel1	$$⊢\left(\phi \wedge x\in X\right)\to AFB$$

Proof

Step	Hyp	Ref	Expression
1		flift.1	$$⊢F=\mathrm{ran}\left(x\in X⟼⟨A,B⟩\right)$$
2		flift.2	$$⊢\left(\phi \wedge x\in X\right)\to A\in R$$
3		flift.3	$$⊢\left(\phi \wedge x\in X\right)\to B\in S$$
4		opex	$$⊢⟨A,B⟩\in \mathrm{V}$$
5		eqid	$$⊢\left(x\in X⟼⟨A,B⟩\right)=\left(x\in X⟼⟨A,B⟩\right)$$
6	5	elrnmpt1	$$⊢\left(x\in X\wedge ⟨A,B⟩\in \mathrm{V}\right)\to ⟨A,B⟩\in \mathrm{ran}\left(x\in X⟼⟨A,B⟩\right)$$
7	4 6	mpan2	$$⊢x\in X\to ⟨A,B⟩\in \mathrm{ran}\left(x\in X⟼⟨A,B⟩\right)$$
8	7	adantl	$$⊢\left(\phi \wedge x\in X\right)\to ⟨A,B⟩\in \mathrm{ran}\left(x\in X⟼⟨A,B⟩\right)$$
9	8 1	eleqtrrdi	$$⊢\left(\phi \wedge x\in X\right)\to ⟨A,B⟩\in F$$
10		df-br	$$⊢AFB\leftrightarrow ⟨A,B⟩\in F$$
11	9 10	sylibr	$$⊢\left(\phi \wedge x\in X\right)\to AFB$$