Theorem opeq1 4202

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

Assertion

Ref	Expression
opeq1	|- ( A = B -> <. A , C >. = <. B , C >. )

Proof of Theorem opeq1

Step	Hyp	Ref	Expression
1		eleq1 2515	. . . 4 |- ( A = B -> ( A e. _V <-> B e. _V ) )
2	1	anbi1d 704	. . 3 |- ( A = B -> ( ( A e. _V /\ C e. _V ) <-> ( B e. _V /\ C e. _V ) ) )
3		sneq 4024	. . . 4 |- ( A = B -> { A } = { B } )
4		preq1 4094	. . . 4 |- ( A = B -> { A , C } = { B , C } )
5	3, 4	preq12d 4102	. . 3 |- ( A = B -> { { A } , { A , C } } = { { B } , { B , C } } )
6	2, 5	ifbieq1d 3949	. 2 |- ( A = B -> if ( ( A e. _V /\ C e. _V ) , { { A } , { A , C } } , (/) ) = if ( ( B e. _V /\ C e. _V ) , { { B } , { B , C } } , (/) ) )
7		dfopif 4199	. 2 |- <. A , C >. = if ( ( A e. _V /\ C e. _V ) , { { A } , { A , C } } , (/) )
8		dfopif 4199	. 2 |- <. B , C >. = if ( ( B e. _V /\ C e. _V ) , { { B } , { B , C } } , (/) )
9	6, 7, 8	3eqtr4g 2509	1 |- ( A = B -> <. A , C >. = <. B , C >. )

Syntax hints:   -> wi 4   /\ wa 369   = wceq 1383   e. wcel 1804   _Vcvv 3095   (/)c0 3770   ifcif 3926   {csn 4014   {cpr 4016   <.cop 4020

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 976  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-rab 2802  df-v 3097  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3771  df-if 3927  df-sn 4015  df-pr 4017  df-op 4021

This theorem is referenced by:  opeq12  4204  opeq1i  4205  opeq1d  4208  oteq1  4211  breq1  4440  cbvopab1  4507  cbvopab1s  4509  opthg  4712  eqvinop  4721  opelopabsb  4747  opelxp  5019  elvvv  5049  opabid2  5122  opeliunxp2  5131  elsnres  5300  elimasng  5353  dmsnopg  5469  cnvsng  5484  funopg  5610  f1osng  5844  f1oprswap  5845  dmfco  5932  fvelrn  6009  fsng  6055  fprg  6065  fvrnressn  6071  fvsng  6090  funfvima3  6134  oveq1  6288  oprabid  6308  dfoprab2  6328  cbvoprab1  6354  elxp4  6729  elxp5  6730  opabex3d  6763  opabex3  6764  op1stg  6797  op2ndg  6798  el2xptp  6828  dfoprab4f  6843  frxp  6895  tfrlem11  7059  omeu  7236  oeeui  7253  elixpsn  7510  fundmen  7591  xpsnen  7603  xpassen  7613  xpf1o  7681  unxpdomlem1  7726  dfac5lem1  8507  dfac5lem4  8510  axdc4lem  8838  nqereu  9310  mulcanenq  9341  archnq  9361  prlem934  9414  supsrlem  9491  supsr  9492  swrdccatin1  12690  swrdccat3blem  12702  fsum2dlem  13567  fprod2dlem  13766  vdwlem10  14490  imasaddfnlem  14907  catideu  15054  iscatd2  15060  catlid  15062  catpropd  15086  symg2bas  16402  efgmval  16709  efgi  16716  vrgpval  16764  gsumcom2  16982  txkgen  20131  cnmpt21  20150  xkoinjcn  20166  txcon  20168  pt1hmeo  20285  cnextfvval  20543  qustgplem  20597  dvbsss  22284  axlowdim2  24241  axlowdim  24242  axcontlem10  24254  axcontlem12  24256  0eusgraiff0rgra  24917  drngoi  25387  isdivrngo  25411  isnvlem  25481  br8d  27441  cnvoprab  27524  prsrn  27875  eulerpartlemgvv  28293  br8  29161  br6  29162  br4  29163  eldm3  29167  dfdm5  29182  elfuns  29541  brimg  29563  brapply  29564  brrestrict  29575  dfrdg4  29576  cgrdegen  29630  brofs  29631  cgrextend  29634  brifs  29669  ifscgr  29670  brcgr3  29672  brcolinear2  29684  colineardim1  29687  brfs  29705  idinside  29710  btwnconn1lem7  29719  btwnconn1lem11  29723  btwnconn1lem12  29724  brsegle  29734  outsideofeu  29757  fvray  29767  linedegen  29769  fvline  29770  dropab1  31310  relopabVD  33569  bj-inftyexpiinv  34486  bj-inftyexpidisj  34488  dicelval3  36782  dihjatcclem4  37023