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

Metamath Proof Explorer

Theorem ecoptocl

Description: Implicit substitution of class for equivalence class of ordered pair. (Contributed by NM, 23-Jul-1995)

Ref Expression
Hypotheses ecoptocl.1 
|- S = ( ( B X. C ) /. R )
ecoptocl.2 
|- ( [ <. x , y >. ] R = A -> ( ph <-> ps ) )
ecoptocl.3 
|- ( ( x e. B /\ y e. C ) -> ph )
Assertion ecoptocl 
|- ( A e. S -> ps )

Proof

Step Hyp Ref Expression
1 ecoptocl.1 
 |-  S = ( ( B X. C ) /. R )
2 ecoptocl.2 
 |-  ( [ <. x , y >. ] R = A -> ( ph <-> ps ) )
3 ecoptocl.3 
 |-  ( ( x e. B /\ y e. C ) -> ph )
4 elqsi 
 |-  ( A e. ( ( B X. C ) /. R ) -> E. z e. ( B X. C ) A = [ z ] R )
5 eqid 
 |-  ( B X. C ) = ( B X. C )
6 eceq1 
 |-  ( <. x , y >. = z -> [ <. x , y >. ] R = [ z ] R )
7 6 eqeq2d 
 |-  ( <. x , y >. = z -> ( A = [ <. x , y >. ] R <-> A = [ z ] R ) )
8 7 imbi1d 
 |-  ( <. x , y >. = z -> ( ( A = [ <. x , y >. ] R -> ps ) <-> ( A = [ z ] R -> ps ) ) )
9 2 eqcoms 
 |-  ( A = [ <. x , y >. ] R -> ( ph <-> ps ) )
10 3 9 syl5ibcom 
 |-  ( ( x e. B /\ y e. C ) -> ( A = [ <. x , y >. ] R -> ps ) )
11 5 8 10 optocl 
 |-  ( z e. ( B X. C ) -> ( A = [ z ] R -> ps ) )
12 11 rexlimiv 
 |-  ( E. z e. ( B X. C ) A = [ z ] R -> ps )
13 4 12 syl 
 |-  ( A e. ( ( B X. C ) /. R ) -> ps )
14 13 1 eleq2s 
 |-  ( A e. S -> ps )