Metamath Proof Explorer

Theorem eldmqsres

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

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

Proof

Step Hyp Ref Expression
1 elqsg 
 |-  ( B e. V -> ( B e. ( dom ( R |` A ) /. ( R |` A ) ) <-> E. u e. dom ( R |` A ) B = [ u ] ( R |` A ) ) )
2 eldmres2 
 |-  ( u e. _V -> ( u e. dom ( R |` A ) <-> ( u e. A /\ E. x x e. [ u ] R ) ) )
3 2 elv 
 |-  ( u e. dom ( R |` A ) <-> ( u e. A /\ E. x x e. [ u ] R ) )
4 3 anbi1i 
 |-  ( ( u e. dom ( R |` A ) /\ B = [ u ] ( R |` A ) ) <-> ( ( u e. A /\ E. x x e. [ u ] R ) /\ B = [ u ] ( R |` A ) ) )
5 ecres2 
 |-  ( u e. A -> [ u ] ( R |` A ) = [ u ] R )
6 5 eqeq2d 
 |-  ( u e. A -> ( B = [ u ] ( R |` A ) <-> B = [ u ] R ) )
7 6 pm5.32i 
 |-  ( ( u e. A /\ B = [ u ] ( R |` A ) ) <-> ( u e. A /\ B = [ u ] R ) )
8 7 anbi2i 
 |-  ( ( E. x x e. [ u ] R /\ ( u e. A /\ B = [ u ] ( R |` A ) ) ) <-> ( E. x x e. [ u ] R /\ ( u e. A /\ B = [ u ] R ) ) )
9 an21 
 |-  ( ( ( u e. A /\ E. x x e. [ u ] R ) /\ B = [ u ] ( R |` A ) ) <-> ( E. x x e. [ u ] R /\ ( u e. A /\ B = [ u ] ( R |` A ) ) ) )
10 an12 
 |-  ( ( u e. A /\ ( E. x x e. [ u ] R /\ B = [ u ] R ) ) <-> ( E. x x e. [ u ] R /\ ( u e. A /\ B = [ u ] R ) ) )
11 8 9 10 3bitr4i 
 |-  ( ( ( u e. A /\ E. x x e. [ u ] R ) /\ B = [ u ] ( R |` A ) ) <-> ( u e. A /\ ( E. x x e. [ u ] R /\ B = [ u ] R ) ) )
12 4 11 bitri 
 |-  ( ( u e. dom ( R |` A ) /\ B = [ u ] ( R |` A ) ) <-> ( u e. A /\ ( E. x x e. [ u ] R /\ B = [ u ] R ) ) )
13 12 rexbii2 
 |-  ( E. u e. dom ( R |` A ) B = [ u ] ( R |` A ) <-> E. u e. A ( E. x x e. [ u ] R /\ B = [ u ] R ) )
14 1 13 bitrdi 
 |-  ( B e. V -> ( B e. ( dom ( R |` A ) /. ( R |` A ) ) <-> E. u e. A ( E. x x e. [ u ] R /\ B = [ u ] R ) ) )