Theorem opeq2 4802

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

Step	Hyp	Ref	Expression
1		eleq1 2826	. . . 4 ⊢ (𝐴 = 𝐵 → (𝐴 ∈ V ↔ 𝐵 ∈ V))
2	1	anbi2d 628	. . 3 ⊢ (𝐴 = 𝐵 → ((𝐶 ∈ V ∧ 𝐴 ∈ V) ↔ (𝐶 ∈ V ∧ 𝐵 ∈ V)))
3		preq2 4667	. . . 4 ⊢ (𝐴 = 𝐵 → {𝐶, 𝐴} = {𝐶, 𝐵})
4	3	preq2d 4673	. . 3 ⊢ (𝐴 = 𝐵 → {{𝐶}, {𝐶, 𝐴}} = {{𝐶}, {𝐶, 𝐵}})
5	2, 4	ifbieq1d 4480	. 2 ⊢ (𝐴 = 𝐵 → if((𝐶 ∈ V ∧ 𝐴 ∈ V), {{𝐶}, {𝐶, 𝐴}}, ∅) = if((𝐶 ∈ V ∧ 𝐵 ∈ V), {{𝐶}, {𝐶, 𝐵}}, ∅))
6		dfopif 4797	. 2 ⊢ ⟨𝐶, 𝐴⟩ = if((𝐶 ∈ V ∧ 𝐴 ∈ V), {{𝐶}, {𝐶, 𝐴}}, ∅)
7		dfopif 4797	. 2 ⊢ ⟨𝐶, 𝐵⟩ = if((𝐶 ∈ V ∧ 𝐵 ∈ V), {{𝐶}, {𝐶, 𝐵}}, ∅)
8	5, 6, 7	3eqtr4g 2804	1 ⊢ (𝐴 = 𝐵 → ⟨𝐶, 𝐴⟩ = ⟨𝐶, 𝐵⟩)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1539   ∈ wcel 2108  Vcvv 3422  ∅c0 4253  ifcif 4456  {csn 4558  {cpr 4560  ⟨cop 4564

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-nul 4254  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565

This theorem is referenced by:  opeq12  4803  opeq2i  4805  opeq2d  4808  oteq2  4811  oteq3  4812  breq2  5074  cbvopab2  5147  cbvopab2v  5151  opthg  5386  eqvinop  5395  opelopabsb  5436  dfid3  5483  opelxp  5616  relopabi  5721  opabid2  5727  elrn2g  5788  opeldmd  5804  opeldm  5805  iss  5932  elidinxp  5940  elimasngOLD  5987  dmsnopg  6105  reuop  6185  funopg  6452  f1osng  6740  f1oprswap  6743  tz6.12f  6780  fvn0ssdmfun  6934  fsn  6989  fsng  6991  fprg  7009  fprb  7051  oveq2  7263  cbvoprab2  7341  ovg  7415  elxp4  7743  elxp5  7744  opabex3d  7781  opabex3rd  7782  opabex3  7783  op1stg  7816  op2ndg  7817  op1steq  7848  dfoprab4f  7869  fsplit  7928  seqomlem2  8252  omeu  8378  oeeui  8395  ralxpmap  8642  elixpsn  8683  ixpsnf1o  8684  mapsnend  8780  xpsnen  8796  xpassen  8806  xpf1o  8875  unxpdomlem1  8956  djulcl  9599  djurcl  9600  djur  9608  djuss  9609  djuun  9615  1stinl  9616  2ndinl  9617  1stinr  9618  2ndinr  9619  axdc4lem  10142  nqereu  10616  mulcanenq  10647  elreal  10818  ax1rid  10848  fseq1p1m1  13259  pfxval  14314  swrdccatin1  14366  swrdccat3blem  14380  wrdlen2  14585  ruclem1  15868  imasaddfnlem  17156  imasvscafn  17165  catidex  17300  catpropd  17335  funcsetcestrclem1  17787  symg2bas  18915  efgi  19240  gsumcom2  19491  mat1rhmval  21536  mat1ric  21544  txkgen  22711  cnmpt21  22730  xkoinjcn  22746  txconn  22748  xpstopnlem1  22868  qustgplem  23180  metustid  23616  axlowdim2  27231  axlowdim  27232  axcontlem2  27236  axcontlem3  27237  axcontlem4  27238  axcontlem9  27243  axcontlem10  27244  axcontlem11  27245  cusgrexg  27714  rgrusgrprc  27859  2clwwlk2clwwlk  28615  isnvlem  28873  br8d  30851  gsumhashmul  31218  prsdm  31766  eulerpartlemgvv  32243  reprsuc  32495  bnj941  32652  bnj944  32818  fineqvrep  32964  cvmlift2lem1  33164  cvmlift2lem12  33176  goel  33209  gonafv  33212  satf0op  33239  sat1el2xp  33241  fmla0xp  33245  sategoelfvb  33281  br8  33629  br6  33630  br4  33631  dfrn5  33654  elima4  33656  xpord2pred  33719  frxp3  33724  xpord3pred  33725  pprodss4v  34113  brimg  34166  brapply  34167  brsuccf  34170  brrestrict  34178  dfrdg4  34180  cgrtriv  34231  brofs  34234  segconeu  34240  btwntriv2  34241  transportprops  34263  brifs  34272  ifscgr  34273  brcgr3  34275  cgrxfr  34284  brcolinear2  34287  colineardim1  34290  brfs  34308  idinside  34313  btwnconn1lem7  34322  btwnconn1lem11  34326  btwnconn1lem12  34327  btwnconn1lem14  34329  brsegle  34337  seglerflx  34341  seglemin  34342  segleantisym  34344  btwnsegle  34346  outsideofeu  34360  outsidele  34361  linedegen  34372  fvline  34373  finxpreclem6  35494  finxpsuclem  35495  curfv  35684  poimirlem4  35708  poimirlem26  35730  isdivrngo  36035  drngoi  36036  iss2  36406  dibelval3  39088  diblsmopel  39112  dihjatcclem4  39362  frlmsnic  40188  dfhe3  41272  dffrege115  41475  dropab2  41955  relopabVD  42410  projf1o  42625  sge0xp  43857  hoidmv1le  44022  fsetsniunop  44430  fsetsnf  44432  fsetsnf1  44433  fsetsnfo  44434  ichnreuop  44812  ichreuopeq  44813  reuopreuprim  44866  0aryfvalel  45868  1arymaptf1  45876  2arymaptf1  45887  prelrrx2b  45948  rrx2xpref1o  45952  rrx2plordisom  45957  isthincd2lem2  46205