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

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

Proof of Theorem opeq1
StepHypRef Expression
1 eleq1 2529 . . . 4
21anbi1d 704 . . 3
3 sneq 4039 . . . 4
4 preq1 4109 . . . 4
53, 4preq12d 4117 . . 3
62, 5ifbieq1d 3964 . 2
7 dfopif 4214 . 2
8 dfopif 4214 . 2
96, 7, 83eqtr4g 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  opeq1i  4220  opeq1d  4223  oteq1  4226  breq1  4455  cbvopab1  4522  cbvopab1s  4524  opthg  4727  eqvinop  4736  opelopabsb  4762  opelxp  5034  elvvv  5064  opabid2  5137  opeliunxp2  5146  elsnres  5315  elimasng  5368  dmsnopg  5484  cnvsng  5499  funopg  5625  f1osng  5859  f1oprswap  5860  dmfco  5947  fvelrn  6024  fsng  6070  fprg  6080  fvrnressn  6086  fvsng  6105  funfvima3  6149  oveq1  6303  oprabid  6323  dfoprab2  6343  cbvoprab1  6369  elxp4  6744  elxp5  6745  opabex3d  6778  opabex3  6779  op1stg  6812  op2ndg  6813  el2xptp  6843  dfoprab4f  6858  frxp  6910  tfrlem11  7076  omeu  7253  oeeui  7270  elixpsn  7528  fundmen  7609  xpsnen  7621  xpassen  7631  xpf1o  7699  unxpdomlem1  7744  dfac5lem1  8525  dfac5lem4  8528  axdc4lem  8856  nqereu  9328  mulcanenq  9359  archnq  9379  prlem934  9432  supsrlem  9509  supsr  9510  swrdccatin1  12708  swrdccat3blem  12720  fsum2dlem  13585  fprod2dlem  13784  vdwlem10  14508  imasaddfnlem  14925  catideu  15072  iscatd2  15078  catlid  15080  catpropd  15104  symg2bas  16423  efgmval  16730  efgi  16737  vrgpval  16785  gsumcom2  17003  txkgen  20153  cnmpt21  20172  xkoinjcn  20188  txcon  20190  pt1hmeo  20307  cnextfvval  20565  qustgplem  20619  dvbsss  22306  axlowdim2  24263  axlowdim  24264  axcontlem10  24276  axcontlem12  24278  0eusgraiff0rgra  24939  drngoi  25409  isdivrngo  25433  isnvlem  25503  br8d  27463  cnvoprab  27546  prsrn  27897  eulerpartlemgvv  28315  br8  29185  br6  29186  br4  29187  eldm3  29191  dfdm5  29206  elfuns  29565  brimg  29587  brapply  29588  brrestrict  29599  dfrdg4  29600  cgrdegen  29654  brofs  29655  cgrextend  29658  brifs  29693  ifscgr  29694  brcgr3  29696  brcolinear2  29708  colineardim1  29711  brfs  29729  idinside  29734  btwnconn1lem7  29743  btwnconn1lem11  29747  btwnconn1lem12  29748  brsegle  29758  outsideofeu  29781  fvray  29791  linedegen  29793  fvline  29794  dropab1  31356  relopabVD  33701  bj-inftyexpiinv  34611  bj-inftyexpidisj  34613  dicelval3  36907  dihjatcclem4  37148
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