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

Metamath Proof Explorer

Theorem eldmqsres2

Description: Elementhood in a restricted domain quotient set. (Contributed by Peter Mazsa, 22-Aug-2020)

Ref Expression
Assertion eldmqsres2 
|- ( B e. V -> ( B e. ( dom ( R |` A ) /. ( R |` A ) ) <-> E. u e. A E. x e. [ u ] R B = [ u ] R ) )

Proof

Step Hyp Ref Expression
1 eldmqsres 
 |-  ( B e. V -> ( B e. ( dom ( R |` A ) /. ( R |` A ) ) <-> E. u e. A ( E. x x e. [ u ] R /\ B = [ u ] R ) ) )
2 df-rex 
 |-  ( E. x e. [ u ] R B = [ u ] R <-> E. x ( x e. [ u ] R /\ B = [ u ] R ) )
3 19.41v 
 |-  ( E. x ( x e. [ u ] R /\ B = [ u ] R ) <-> ( E. x x e. [ u ] R /\ B = [ u ] R ) )
4 2 3 bitri 
 |-  ( E. x e. [ u ] R B = [ u ] R <-> ( E. x x e. [ u ] R /\ B = [ u ] R ) )
5 4 rexbii 
 |-  ( E. u e. A E. x e. [ u ] R B = [ u ] R <-> E. u e. A ( E. x x e. [ u ] R /\ B = [ u ] R ) )
6 1 5 bitr4di 
 |-  ( B e. V -> ( B e. ( dom ( R |` A ) /. ( R |` A ) ) <-> E. u e. A E. x e. [ u ] R B = [ u ] R ) )