Theorem opeq2 4805

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 629	. . 3 ⊢ (𝐴 = 𝐵 → ((𝐶 ∈ V ∧ 𝐴 ∈ V) ↔ (𝐶 ∈ V ∧ 𝐵 ∈ V)))
3		preq2 4670	. . . 4 ⊢ (𝐴 = 𝐵 → {𝐶, 𝐴} = {𝐶, 𝐵})
4	3	preq2d 4676	. . 3 ⊢ (𝐴 = 𝐵 → {{𝐶}, {𝐶, 𝐴}} = {{𝐶}, {𝐶, 𝐵}})
5	2, 4	ifbieq1d 4483	. 2 ⊢ (𝐴 = 𝐵 → if((𝐶 ∈ V ∧ 𝐴 ∈ V), {{𝐶}, {𝐶, 𝐴}}, ∅) = if((𝐶 ∈ V ∧ 𝐵 ∈ V), {{𝐶}, {𝐶, 𝐵}}, ∅))
6		dfopif 4800	. 2 ⊢ ⟨𝐶, 𝐴⟩ = if((𝐶 ∈ V ∧ 𝐴 ∈ V), {{𝐶}, {𝐶, 𝐴}}, ∅)
7		dfopif 4800	. 2 ⊢ ⟨𝐶, 𝐵⟩ = if((𝐶 ∈ V ∧ 𝐵 ∈ V), {{𝐶}, {𝐶, 𝐵}}, ∅)
8	5, 6, 7	3eqtr4g 2803	1 ⊢ (𝐴 = 𝐵 → ⟨𝐶, 𝐴⟩ = ⟨𝐶, 𝐵⟩)

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1539   ∈ wcel 2106  Vcvv 3432  ∅c0 4256  ifcif 4459  {csn 4561  {cpr 4563  ⟨cop 4567

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-rab 3073  df-v 3434  df-dif 3890  df-un 3892  df-nul 4257  df-if 4460  df-sn 4562  df-pr 4564  df-op 4568

This theorem is referenced by:  opeq12  4806  opeq2i  4808  opeq2d  4811  oteq2  4814  oteq3  4815  breq2  5078  cbvopab2  5151  cbvopab2v  5155  opthg  5392  eqvinop  5401  opelopabsb  5443  dfid3  5492  opelxp  5625  relopabi  5732  opabid2  5738  elrn2g  5799  opeldmd  5815  opeldm  5816  iss  5943  elidinxp  5951  elimasngOLD  5998  dmsnopg  6116  reuop  6196  funopg  6468  f1osng  6757  f1oprswap  6760  tz6.12f  6798  fvn0ssdmfun  6952  fsn  7007  fsng  7009  fprg  7027  fprb  7069  oveq2  7283  cbvoprab2  7363  ovg  7437  elxp4  7769  elxp5  7770  opabex3d  7808  opabex3rd  7809  opabex3  7810  op1stg  7843  op2ndg  7844  op1steq  7875  dfoprab4f  7896  fsplit  7957  seqomlem2  8282  omeu  8416  oeeui  8433  ralxpmap  8684  elixpsn  8725  ixpsnf1o  8726  mapsnend  8826  xpsnen  8842  xpassen  8853  xpf1o  8926  unxpdomlem1  9027  djulcl  9668  djurcl  9669  djur  9677  djuss  9678  djuun  9684  1stinl  9685  2ndinl  9686  1stinr  9687  2ndinr  9688  axdc4lem  10211  nqereu  10685  mulcanenq  10716  elreal  10887  ax1rid  10917  fseq1p1m1  13330  pfxval  14386  swrdccatin1  14438  swrdccat3blem  14452  wrdlen2  14657  ruclem1  15940  imasaddfnlem  17239  imasvscafn  17248  catidex  17383  catpropd  17418  funcsetcestrclem1  17871  symg2bas  19000  efgi  19325  gsumcom2  19576  mat1rhmval  21628  mat1ric  21636  txkgen  22803  cnmpt21  22822  xkoinjcn  22838  txconn  22840  xpstopnlem1  22960  qustgplem  23272  metustid  23710  axlowdim2  27328  axlowdim  27329  axcontlem2  27333  axcontlem3  27334  axcontlem4  27335  axcontlem9  27340  axcontlem10  27341  axcontlem11  27342  cusgrexg  27811  rgrusgrprc  27956  2clwwlk2clwwlk  28714  isnvlem  28972  br8d  30950  gsumhashmul  31316  prsdm  31864  eulerpartlemgvv  32343  reprsuc  32595  bnj941  32752  bnj944  32918  fineqvrep  33064  cvmlift2lem1  33264  cvmlift2lem12  33276  goel  33309  gonafv  33312  satf0op  33339  sat1el2xp  33341  fmla0xp  33345  sategoelfvb  33381  br8  33723  br6  33724  br4  33725  dfrn5  33748  elima4  33750  xpord2pred  33792  frxp3  33797  xpord3pred  33798  pprodss4v  34186  brimg  34239  brapply  34240  brsuccf  34243  brrestrict  34251  dfrdg4  34253  cgrtriv  34304  brofs  34307  segconeu  34313  btwntriv2  34314  transportprops  34336  brifs  34345  ifscgr  34346  brcgr3  34348  cgrxfr  34357  brcolinear2  34360  colineardim1  34363  brfs  34381  idinside  34386  btwnconn1lem7  34395  btwnconn1lem11  34399  btwnconn1lem12  34400  btwnconn1lem14  34402  brsegle  34410  seglerflx  34414  seglemin  34415  segleantisym  34417  btwnsegle  34419  outsideofeu  34433  outsidele  34434  linedegen  34445  fvline  34446  finxpreclem6  35567  finxpsuclem  35568  curfv  35757  poimirlem4  35781  poimirlem26  35803  isdivrngo  36108  drngoi  36109  iss2  36479  dibelval3  39161  diblsmopel  39185  dihjatcclem4  39435  frlmsnic  40263  dfhe3  41383  dffrege115  41586  dropab2  42066  relopabVD  42521  projf1o  42736  sge0xp  43967  hoidmv1le  44132  fsetsniunop  44543  fsetsnf  44545  fsetsnf1  44546  fsetsnfo  44547  ichnreuop  44924  ichreuopeq  44925  reuopreuprim  44978  0aryfvalel  45980  1arymaptf1  45988  2arymaptf1  45999  prelrrx2b  46060  rrx2xpref1o  46064  rrx2plordisom  46069  isthincd2lem2  46317