ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  opeq2 Unicode version

Theorem opeq2 3712
Description: Equality theorem for ordered pairs. (Contributed by NM, 25-Jun-1998.) (Revised by Mario Carneiro, 26-Apr-2015.)
Assertion
Ref Expression
opeq2  |-  ( A  =  B  ->  <. C ,  A >.  =  <. C ,  B >. )

Proof of Theorem opeq2
Dummy variable  x is distinct from all other variables.
StepHypRef Expression
1 eleq1 2203 . . . . . 6  |-  ( A  =  B  ->  ( A  e.  _V  <->  B  e.  _V ) )
21anbi2d 460 . . . . 5  |-  ( A  =  B  ->  (
( C  e.  _V  /\  A  e.  _V )  <->  ( C  e.  _V  /\  B  e.  _V )
) )
3 eqidd 2141 . . . . . . 7  |-  ( A  =  B  ->  { C }  =  { C } )
4 preq2 3607 . . . . . . 7  |-  ( A  =  B  ->  { C ,  A }  =  { C ,  B }
)
53, 4preq12d 3614 . . . . . 6  |-  ( A  =  B  ->  { { C } ,  { C ,  A } }  =  { { C } ,  { C ,  B } } )
65eleq2d 2210 . . . . 5  |-  ( A  =  B  ->  (
x  e.  { { C } ,  { C ,  A } }  <->  x  e.  { { C } ,  { C ,  B } } ) )
72, 6anbi12d 465 . . . 4  |-  ( A  =  B  ->  (
( ( C  e. 
_V  /\  A  e.  _V )  /\  x  e.  { { C } ,  { C ,  A } } )  <->  ( ( C  e.  _V  /\  B  e.  _V )  /\  x  e.  { { C } ,  { C ,  B } } ) ) )
8 df-3an 965 . . . 4  |-  ( ( C  e.  _V  /\  A  e.  _V  /\  x  e.  { { C } ,  { C ,  A } } )  <->  ( ( C  e.  _V  /\  A  e.  _V )  /\  x  e.  { { C } ,  { C ,  A } } ) )
9 df-3an 965 . . . 4  |-  ( ( C  e.  _V  /\  B  e.  _V  /\  x  e.  { { C } ,  { C ,  B } } )  <->  ( ( C  e.  _V  /\  B  e.  _V )  /\  x  e.  { { C } ,  { C ,  B } } ) )
107, 8, 93bitr4g 222 . . 3  |-  ( A  =  B  ->  (
( C  e.  _V  /\  A  e.  _V  /\  x  e.  { { C } ,  { C ,  A } } )  <-> 
( C  e.  _V  /\  B  e.  _V  /\  x  e.  { { C } ,  { C ,  B } } ) ) )
1110abbidv 2258 . 2  |-  ( A  =  B  ->  { x  |  ( C  e. 
_V  /\  A  e.  _V  /\  x  e.  { { C } ,  { C ,  A } } ) }  =  { x  |  ( C  e.  _V  /\  B  e.  _V  /\  x  e. 
{ { C } ,  { C ,  B } } ) } )
12 df-op 3539 . 2  |-  <. C ,  A >.  =  { x  |  ( C  e. 
_V  /\  A  e.  _V  /\  x  e.  { { C } ,  { C ,  A } } ) }
13 df-op 3539 . 2  |-  <. C ,  B >.  =  { x  |  ( C  e. 
_V  /\  B  e.  _V  /\  x  e.  { { C } ,  { C ,  B } } ) }
1411, 12, 133eqtr4g 2198 1  |-  ( A  =  B  ->  <. C ,  A >.  =  <. C ,  B >. )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 103    /\ w3a 963    = wceq 1332    e. wcel 1481   {cab 2126   _Vcvv 2689   {csn 3530   {cpr 3531   <.cop 3533
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-10 1484  ax-11 1485  ax-i12 1486  ax-bndl 1487  ax-4 1488  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122
This theorem depends on definitions:  df-bi 116  df-3an 965  df-tru 1335  df-nf 1438  df-sb 1737  df-clab 2127  df-cleq 2133  df-clel 2136  df-nfc 2271  df-v 2691  df-un 3078  df-sn 3536  df-pr 3537  df-op 3539
This theorem is referenced by:  opeq12  3713  opeq2i  3715  opeq2d  3718  oteq2  3721  oteq3  3722  breq2  3939  cbvopab2  4008  cbvopab2v  4011  opthg  4166  eqvinop  4171  opelopabsb  4188  opelxp  4575  opabid2  4676  elrn2g  4735  opeldm  4748  opeldmg  4750  elrn2  4787  opelresg  4832  iss  4871  elimasng  4913  issref  4927  dmsnopg  5016  cnvsng  5030  elxp4  5032  elxp5  5033  dffun5r  5141  funopg  5163  f1osng  5414  tz6.12f  5456  fsn  5598  fsng  5599  fvsng  5622  oveq2  5788  cbvoprab2  5850  ovg  5915  opabex3d  6025  opabex3  6026  op1stg  6054  op2ndg  6055  oprssdmm  6075  op1steq  6083  dfoprab4f  6097  tfrlemibxssdm  6230  tfr1onlembxssdm  6246  tfrcllembxssdm  6259  elixpsn  6635  ixpsnf1o  6636  mapsnen  6711  xpsnen  6721  xpassen  6730  xpf1o  6744  djulclr  6940  djurclr  6941  djulcl  6942  djurcl  6943  djulclb  6946  inl11  6956  djuss  6961  1stinl  6965  2ndinl  6966  1stinr  6967  2ndinr  6968  elreal  7658  ax1rid  7707  fseq1p1m1  9903  cnmpt21  12492  djucllem  13171
  Copyright terms: Public domain W3C validator