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

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

Proof of Theorem opeq1
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 eleq1 2100 . . . . . 6  _V  _V
21anbi1d 438 . . . . 5  _V  C  _V  _V  C  _V
3 sneq 3381 . . . . . . 7  { }  { }
4 preq1 3441 . . . . . . 7  { ,  C }  { ,  C }
53, 4preq12d 3449 . . . . . 6  { { } ,  { ,  C } }  { { } ,  { ,  C } }
65eleq2d 2107 . . . . 5  { { } ,  { ,  C } } 
{ { } ,  { ,  C } }
72, 6anbi12d 442 . . . 4  _V  C  _V  { { } ,  { ,  C } }  _V  C  _V  { { } ,  { ,  C } }
8 df-3an 887 . . . 4  _V  C  _V  { { } ,  { ,  C } }  _V  C  _V  { { } ,  { ,  C } }
9 df-3an 887 . . . 4  _V  C  _V  { { } ,  { ,  C } }  _V  C  _V  { { } ,  { ,  C } }
107, 8, 93bitr4g 212 . . 3  _V  C  _V  { { } ,  { ,  C } }  _V  C  _V  { { } ,  { ,  C } }
1110abbidv 2155 . 2  {  |  _V  C 
_V  { { } ,  { ,  C } } }  {  |  _V  C  _V 
{ { } ,  { ,  C } } }
12 df-op 3379 . 2  <. ,  C >.  {  |  _V  C  _V  { { } ,  { ,  C } } }
13 df-op 3379 . 2  <. ,  C >.  {  |  _V  C  _V  { { } ,  { ,  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  opeq1i  3546  opeq1d  3549  oteq1  3552  breq1  3761  cbvopab1  3824  cbvopab1s  3826  opthg  3969  eqvinop  3974  opelopabsb  3991  opelxp  4320  elvvv  4349  opabid2  4413  opeliunxp2  4422  elsnres  4593  elimasng  4639  rnxpid  4701  dmsnopg  4738  cnvsng  4752  elxp4  4754  elxp5  4755  funopg  4880  f1osng  5113  dmfco  5187  fvelrn  5244  fsng  5282  fvsng  5305  funfvima3  5338  oveq1  5465  oprabid  5483  dfoprab2  5497  cbvoprab1  5521  opabex3d  5693  opabex3  5694  op1stg  5722  op2ndg  5723  dfoprab4f  5764  fundmen  6225  xpsnen  6234  xpassen  6243  ltexnqq  6395  archnqq  6404  prarloclemarch2  6406  prarloclemlo  6481  prarloclem3  6484  prarloclem5  6487  caucvgprlemnkj  6653  caucvgprlemnbj  6654  caucvgprlemm  6655  caucvgprlemdisj  6661  caucvgprlemloc  6662  caucvgprlemcl  6663  caucvgprlemladdfu  6664  caucvgprlemladdrl  6665  caucvgprlem1  6666  caucvgprlem2  6667  caucvgpr  6669  caucvgprprlemell  6672  caucvgprprlemelu  6673  caucvgprprlemcbv  6674  caucvgprprlemval  6675  caucvgprprlemnkeqj  6677  caucvgprprlemmu  6682  caucvgprprlemopl  6684  caucvgprprlemlol  6685  caucvgprprlemopu  6686  caucvgprprlemloc  6690  caucvgprprlemclphr  6692  caucvgprprlemexbt  6693  caucvgprprlem1  6696  caucvgprprlem2  6697  caucvgsr  6775  elrealeu  6795  pitonn  6813  nntopi  6857  axcaucvglemval  6860  axcaucvg  6863
  Copyright terms: Public domain W3C validator