Theorem fliftel1

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

	Ref	Expression
Hypotheses	flift.1	⊢ 𝐹 = ran ( 𝑥 ∈ 𝑋 ↦ ⟨ 𝐴 , 𝐵 ⟩ )
	flift.2	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐴 ∈ 𝑅 )
	flift.3	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐵 ∈ 𝑆 )
Assertion	fliftel1	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐴 𝐹 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		flift.1	⊢ 𝐹 = ran ( 𝑥 ∈ 𝑋 ↦ ⟨ 𝐴 , 𝐵 ⟩ )
2		flift.2	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐴 ∈ 𝑅 )
3		flift.3	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐵 ∈ 𝑆 )
4		opex	⊢ ⟨ 𝐴 , 𝐵 ⟩ ∈ V
5		eqid	⊢ ( 𝑥 ∈ 𝑋 ↦ ⟨ 𝐴 , 𝐵 ⟩ ) = ( 𝑥 ∈ 𝑋 ↦ ⟨ 𝐴 , 𝐵 ⟩ )
6	5	elrnmpt1	⊢ ( ( 𝑥 ∈ 𝑋 ∧ ⟨ 𝐴 , 𝐵 ⟩ ∈ V ) → ⟨ 𝐴 , 𝐵 ⟩ ∈ ran ( 𝑥 ∈ 𝑋 ↦ ⟨ 𝐴 , 𝐵 ⟩ ) )
7	4 6	mpan2	⊢ ( 𝑥 ∈ 𝑋 → ⟨ 𝐴 , 𝐵 ⟩ ∈ ran ( 𝑥 ∈ 𝑋 ↦ ⟨ 𝐴 , 𝐵 ⟩ ) )
8	7	adantl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ⟨ 𝐴 , 𝐵 ⟩ ∈ ran ( 𝑥 ∈ 𝑋 ↦ ⟨ 𝐴 , 𝐵 ⟩ ) )
9	8 1	eleqtrrdi	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ⟨ 𝐴 , 𝐵 ⟩ ∈ 𝐹 )
10		df-br	⊢ ( 𝐴 𝐹 𝐵 ↔ ⟨ 𝐴 , 𝐵 ⟩ ∈ 𝐹 )
11	9 10	sylibr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐴 𝐹 𝐵 )