# Metamath Proof Explorer

## 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 {A}{F}{B}$

### 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 ${⊢}{A}{F}{B}↔⟨{A},{B}⟩\in {F}$
11 9 10 sylibr ${⊢}\left({\phi }\wedge {x}\in {X}\right)\to {A}{F}{B}$