Metamath Proof Explorer

Theorem ecelqsdm

Description: Membership of an equivalence class in a quotient set. (Contributed by NM, 30-Jul-1995)

Ref Expression
Assertion ecelqsdm 
|- ( ( dom R = A /\ [ B ] R e. ( A /. R ) ) -> B e. A )

Proof

Step Hyp Ref Expression
1 elqsn0 
 |-  ( ( dom R = A /\ [ B ] R e. ( A /. R ) ) -> [ B ] R =/= (/) )
2 ecdmn0 
 |-  ( B e. dom R <-> [ B ] R =/= (/) )
3 1 2 sylibr 
 |-  ( ( dom R = A /\ [ B ] R e. ( A /. R ) ) -> B e. dom R )
4 simpl 
 |-  ( ( dom R = A /\ [ B ] R e. ( A /. R ) ) -> dom R = A )
5 3 4 eleqtrd 
 |-  ( ( dom R = A /\ [ B ] R e. ( A /. R ) ) -> B e. A )