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 )