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

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

Proof of Theorem opeq2
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 eleq1 2100 . . . . . 6  _V  _V
21anbi2d 437 . . . . 5  C  _V  _V  C  _V  _V
3 eqidd 2041 . . . . . . 7  { C }  { C }
4 preq2 3442 . . . . . . 7  { C ,  }  { C ,  }
53, 4preq12d 3449 . . . . . 6  { { C } ,  { C ,  } }  { { C } ,  { C ,  } }
65eleq2d 2107 . . . . 5  { { C } ,  { C ,  } } 
{ { C } ,  { C ,  } }
72, 6anbi12d 442 . . . 4  C  _V  _V  { { C } ,  { C ,  } }  C 
_V  _V  { { C } ,  { C ,  } }
8 df-3an 887 . . . 4  C  _V  _V  { { C } ,  { C ,  } }  C  _V  _V  { { C } ,  { C ,  } }
9 df-3an 887 . . . 4  C  _V  _V  { { C } ,  { C ,  } }  C  _V  _V  { { C } ,  { C ,  } }
107, 8, 93bitr4g 212 . . 3  C  _V  _V  { { C } ,  { C ,  } }  C  _V  _V  { { C } ,  { C ,  } }
1110abbidv 2155 . 2  {  |  C  _V  _V  { { C } ,  { C ,  } } }  {  |  C  _V  _V 
{ { C } ,  { C ,  } } }
12 df-op 3379 . 2  <. C ,  >.  {  |  C  _V  _V  { { C } ,  { C ,  } } }
13 df-op 3379 . 2  <. C ,  >.  {  |  C  _V  _V  { { C } ,  { C ,  } } }
1411, 12, 133eqtr4g 2097 1  <. C ,  >.  <. C ,  >.
Colors of variables: wff set class
Syntax hints:   wi 4   wa 97   w3a 885   wceq 1243   wcel 1393   {cab 2026   _Vcvv 2554   {csn 3370   {cpr 3371   <.cop 3373
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 630  ax-5 1336  ax-7 1337  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-8 1395  ax-10 1396  ax-11 1397  ax-i12 1398  ax-bndl 1399  ax-4 1400  ax-17 1419  ax-i9 1423  ax-ial 1427  ax-i5r 1428  ax-ext 2022
This theorem depends on definitions:  df-bi 110  df-3an 887  df-tru 1246  df-nf 1350  df-sb 1646  df-clab 2027  df-cleq 2033  df-clel 2036  df-nfc 2167  df-v 2556  df-un 2919  df-sn 3376  df-pr 3377  df-op 3379
This theorem is referenced by:  opeq12  3545  opeq2i  3547  opeq2d  3550  oteq2  3553  oteq3  3554  breq2  3762  cbvopab2  3825  cbvopab2v  3828  opthg  3969  eqvinop  3974  opelopabsb  3991  opelxp  4320  opabid2  4413  elrn2g  4471  opeldm  4484  opeldmg  4486  elrn2  4522  opelresg  4565  iss  4600  elimasng  4639  issref  4653  dmsnopg  4738  cnvsng  4752  elxp4  4754  elxp5  4755  dffun5r  4860  funopg  4880  f1osng  5113  tz6.12f  5148  fsn  5281  fsng  5282  fvsng  5305  oveq2  5466  cbvoprab2  5522  ovg  5584  opabex3d  5693  opabex3  5694  op1stg  5722  op2ndg  5723  op1steq  5750  dfoprab4f  5764  tfrlemibxssdm  5886  xpsnen  6235  xpassen  6244  elreal  6795  ax1rid  6841  fseq1p1m1  8818
  Copyright terms: Public domain W3C validator