Theorem fliftel1

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

	Ref	Expression
Hypotheses	flift.1	|- F = ran ( x e. X |-> <. A , B >. )
	flift.2	|- ( ( ph /\ x e. X ) -> A e. R )
	flift.3	|- ( ( ph /\ x e. X ) -> B e. S )
Assertion	fliftel1	|- ( ( ph /\ x e. X ) -> A F B )

Proof

Step	Hyp	Ref	Expression
1		flift.1	|- F = ran ( x e. X |-> <. A , B >. )
2		flift.2	|- ( ( ph /\ x e. X ) -> A e. R )
3		flift.3	|- ( ( ph /\ x e. X ) -> B e. S )
4		opex	|- <. A , B >. e. _V
5		eqid	|- ( x e. X |-> <. A , B >. ) = ( x e. X |-> <. A , B >. )
6	5	elrnmpt1	|- ( ( x e. X /\ <. A , B >. e. _V ) -> <. A , B >. e. ran ( x e. X |-> <. A , B >. ) )
7	4 6	mpan2	|- ( x e. X -> <. A , B >. e. ran ( x e. X |-> <. A , B >. ) )
8	7	adantl	|- ( ( ph /\ x e. X ) -> <. A , B >. e. ran ( x e. X |-> <. A , B >. ) )
9	8 1	eleqtrrdi	|- ( ( ph /\ x e. X ) -> <. A , B >. e. F )
10		df-br	|- ( A F B <-> <. A , B >. e. F )
11	9 10	sylibr	|- ( ( ph /\ x e. X ) -> A F B )