MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  opeq2 Unicode version

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

Proof of Theorem opeq2
StepHypRef Expression
1 eleq1 2529 . . . 4
21anbi2d 703 . . 3
3 preq2 4110 . . . 4
43preq2d 4116 . . 3
52, 4ifbieq1d 3964 . 2
6 dfopif 4214 . 2
7 dfopif 4214 . 2
85, 6, 73eqtr4g 2523 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 369  =wceq 1395  e.wcel 1818   cvv 3109   c0 3784  ifcif 3941  {csn 4029  {cpr 4031  <.cop 4035
This theorem is referenced by:  opeq12  4219  opeq2i  4221  opeq2d  4224  oteq2  4227  oteq3  4228  breq2  4456  cbvopab2  4523  cbvopab2v  4526  opthg  4727  eqvinop  4736  opelopabsb  4762  dfid3  4801  opelxp  5034  opabid2  5137  elrn2g  5198  opeldm  5211  elrn2  5247  opelresg  5286  iss  5326  elimasng  5368  issref  5385  dmsnopg  5484  cnvsng  5499  funopg  5625  f1osng  5859  f1oprswap  5860  tz6.12f  5889  fvn0ssdmfun  6022  fsn  6069  fsng  6070  fprg  6080  fvsng  6105  oveq2  6304  cbvoprab2  6370  ovg  6441  elxp4  6744  elxp5  6745  opabex3d  6778  opabex3  6779  op1stg  6812  op2ndg  6813  op1steq  6842  dfoprab4f  6858  seqomlem2  7135  omeu  7253  oeeui  7270  ralxpmap  7488  elixpsn  7528  ixpsnf1o  7529  mapsnen  7613  xpsnen  7621  xpassen  7631  xpf1o  7699  unxpdomlem1  7744  axdc4lem  8856  nqereu  9328  mulcanenq  9359  elreal  9529  ax1rid  9559  fseq1p1m1  11781  swrdccatin1  12708  swrdccat3blem  12720  swrdccatid  12722  swrdccatin12d  12726  wrdlen2  12886  ruclem1  13964  imasaddfnlem  14925  imasvscafn  14934  catidex  15071  catpropd  15104  symg2bas  16423  psgnunilem5  16519  efgi  16737  gsumcom2  17003  mat1rhmval  18981  mat1ric  18989  txkgen  20153  cnmpt21  20172  xkoinjcn  20188  txcon  20190  xpstopnlem1  20310  qustgplem  20619  metustidOLD  21062  metustid  21063  axlowdim2  24263  axlowdim  24264  axcontlem2  24268  axcontlem3  24269  axcontlem4  24270  axcontlem9  24275  axcontlem10  24276  axcontlem11  24277  1pthoncl  24594  2pthoncl  24605  wwlknextbi  24725  wwlkextinj  24730  wwlkextsur  24731  clwwlkfo  24797  0eusgraiff0rgra  24939  drngoi  25409  isdivrngo  25433  vcoprne  25472  isnvlem  25503  br8d  27463  prsdm  27896  eulerpartlemgvv  28315  cvmlift2lem1  28747  cvmlift2lem12  28759  br8  29185  br6  29186  br4  29187  fprb  29203  dfrn5  29207  elima4  29209  pprodss4v  29534  brimg  29587  brapply  29588  brrestrict  29599  dfrdg4  29600  cgrtriv  29652  brofs  29655  segconeu  29661  btwntriv2  29662  transportprops  29684  brifs  29693  ifscgr  29694  brcgr3  29696  cgrxfr  29705  brcolinear2  29708  colineardim1  29711  brfs  29729  idinside  29734  btwnconn1lem7  29743  btwnconn1lem11  29747  btwnconn1lem12  29748  btwnconn1lem14  29750  brsegle  29758  seglerflx  29762  seglemin  29763  segleantisym  29765  btwnsegle  29767  outsideofeu  29781  outsidele  29782  linedegen  29793  fvline  29794  dropab2  31357  funcsetcestrclem1  32660  relopabVD  33701  bnj941  33831  bnj944  33996  dibelval3  36874  diblsmopel  36898  dihjatcclem4  37148  dfhe3  37799
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-rab 2816  df-v 3111  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-nul 3785  df-if 3942  df-sn 4030  df-pr 4032  df-op 4036
  Copyright terms: Public domain W3C validator