Metamath Proof Explorer

Theorem eldmqs1cossres

Description: Elementhood in the domain quotient of the class of cosets by a restriction. (Contributed by Peter Mazsa, 4-May-2019)

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

Proof

Step Hyp Ref Expression
1 elqsg 
 |-  ( B e. V -> ( B e. ( dom ,~ ( R |` A ) /. ,~ ( R |` A ) ) <-> E. x e. dom ,~ ( R |` A ) B = [ x ] ,~ ( R |` A ) ) )
2 df-rex 
 |-  ( E. x e. dom ,~ ( R |` A ) B = [ x ] ,~ ( R |` A ) <-> E. x ( x e. dom ,~ ( R |` A ) /\ B = [ x ] ,~ ( R |` A ) ) )
3 eldm1cossres2 
 |-  ( x e. _V -> ( x e. dom ,~ ( R |` A ) <-> E. u e. A x e. [ u ] R ) )
4 3 elv 
 |-  ( x e. dom ,~ ( R |` A ) <-> E. u e. A x e. [ u ] R )
5 4 anbi1i 
 |-  ( ( x e. dom ,~ ( R |` A ) /\ B = [ x ] ,~ ( R |` A ) ) <-> ( E. u e. A x e. [ u ] R /\ B = [ x ] ,~ ( R |` A ) ) )
6 5 exbii 
 |-  ( E. x ( x e. dom ,~ ( R |` A ) /\ B = [ x ] ,~ ( R |` A ) ) <-> E. x ( E. u e. A x e. [ u ] R /\ B = [ x ] ,~ ( R |` A ) ) )
7 2 6 bitri 
 |-  ( E. x e. dom ,~ ( R |` A ) B = [ x ] ,~ ( R |` A ) <-> E. x ( E. u e. A x e. [ u ] R /\ B = [ x ] ,~ ( R |` A ) ) )
8 1 7 bitrdi 
 |-  ( B e. V -> ( B e. ( dom ,~ ( R |` A ) /. ,~ ( R |` A ) ) <-> E. x ( E. u e. A x e. [ u ] R /\ B = [ x ] ,~ ( R |` A ) ) ) )
9 df-rex 
 |-  ( E. x e. [ u ] R B = [ x ] ,~ ( R |` A ) <-> E. x ( x e. [ u ] R /\ B = [ x ] ,~ ( R |` A ) ) )
10 9 rexbii 
 |-  ( E. u e. A E. x e. [ u ] R B = [ x ] ,~ ( R |` A ) <-> E. u e. A E. x ( x e. [ u ] R /\ B = [ x ] ,~ ( R |` A ) ) )
11 rexcom4 
 |-  ( E. u e. A E. x ( x e. [ u ] R /\ B = [ x ] ,~ ( R |` A ) ) <-> E. x E. u e. A ( x e. [ u ] R /\ B = [ x ] ,~ ( R |` A ) ) )
12 r19.41v 
 |-  ( E. u e. A ( x e. [ u ] R /\ B = [ x ] ,~ ( R |` A ) ) <-> ( E. u e. A x e. [ u ] R /\ B = [ x ] ,~ ( R |` A ) ) )
13 12 exbii 
 |-  ( E. x E. u e. A ( x e. [ u ] R /\ B = [ x ] ,~ ( R |` A ) ) <-> E. x ( E. u e. A x e. [ u ] R /\ B = [ x ] ,~ ( R |` A ) ) )
14 11 13 bitri 
 |-  ( E. u e. A E. x ( x e. [ u ] R /\ B = [ x ] ,~ ( R |` A ) ) <-> E. x ( E. u e. A x e. [ u ] R /\ B = [ x ] ,~ ( R |` A ) ) )
15 10 14 bitri 
 |-  ( E. u e. A E. x e. [ u ] R B = [ x ] ,~ ( R |` A ) <-> E. x ( E. u e. A x e. [ u ] R /\ B = [ x ] ,~ ( R |` A ) ) )
16 8 15 bitr4di 
 |-  ( B e. V -> ( B e. ( dom ,~ ( R |` A ) /. ,~ ( R |` A ) ) <-> E. u e. A E. x e. [ u ] R B = [ x ] ,~ ( R |` A ) ) )