This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem qliftel

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 = ran ( x e. X |-> <. [ x ] R , A >. )
qlift.2 
|- ( ( ph /\ x e. X ) -> A e. Y )
qlift.3 
|- ( ph -> R Er X )
qlift.4 
|- ( ph -> X e. V )
Assertion qliftel 
|- ( ph -> ( [ C ] R F D <-> E. x e. X ( C R x /\ D = A ) ) )

Proof

Step Hyp Ref Expression
1 qlift.1 
 |-  F = ran ( x e. X |-> <. [ x ] R , A >. )
2 qlift.2 
 |-  ( ( ph /\ x e. X ) -> A e. Y )
3 qlift.3 
 |-  ( ph -> R Er X )
4 qlift.4 
 |-  ( ph -> X e. V )
5 1 2 3 4 qliftlem 
 |-  ( ( ph /\ x e. X ) -> [ x ] R e. ( X /. R ) )
6 1 5 2 fliftel 
 |-  ( ph -> ( [ C ] R F D <-> E. x e. X ( [ C ] R = [ x ] R /\ D = A ) ) )
7 3 adantr 
 |-  ( ( ph /\ x e. X ) -> R Er X )
8 simpr 
 |-  ( ( ph /\ x e. X ) -> x e. X )
9 7 8 erth2 
 |-  ( ( ph /\ x e. X ) -> ( C R x <-> [ C ] R = [ x ] R ) )
10 9 anbi1d 
 |-  ( ( ph /\ x e. X ) -> ( ( C R x /\ D = A ) <-> ( [ C ] R = [ x ] R /\ D = A ) ) )
11 10 rexbidva 
 |-  ( ph -> ( E. x e. X ( C R x /\ D = A ) <-> E. x e. X ( [ C ] R = [ x ] R /\ D = A ) ) )
12 6 11 bitr4d 
 |-  ( ph -> ( [ C ] R F D <-> E. x e. X ( C R x /\ D = A ) ) )