Theorem opeq2 4830

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 2824	. . . 4 ⊢ (𝐴 = 𝐵 → (𝐴 ∈ V ↔ 𝐵 ∈ V))
2	1	anbi2d 630	. . 3 ⊢ (𝐴 = 𝐵 → ((𝐶 ∈ V ∧ 𝐴 ∈ V) ↔ (𝐶 ∈ V ∧ 𝐵 ∈ V)))
3		preq2 4691	. . . 4 ⊢ (𝐴 = 𝐵 → {𝐶, 𝐴} = {𝐶, 𝐵})
4	3	preq2d 4697	. . 3 ⊢ (𝐴 = 𝐵 → {{𝐶}, {𝐶, 𝐴}} = {{𝐶}, {𝐶, 𝐵}})
5	2, 4	ifbieq1d 4504	. 2 ⊢ (𝐴 = 𝐵 → if((𝐶 ∈ V ∧ 𝐴 ∈ V), {{𝐶}, {𝐶, 𝐴}}, ∅) = if((𝐶 ∈ V ∧ 𝐵 ∈ V), {{𝐶}, {𝐶, 𝐵}}, ∅))
6		dfopif 4826	. 2 ⊢ ⟨𝐶, 𝐴⟩ = if((𝐶 ∈ V ∧ 𝐴 ∈ V), {{𝐶}, {𝐶, 𝐴}}, ∅)
7		dfopif 4826	. 2 ⊢ ⟨𝐶, 𝐵⟩ = if((𝐶 ∈ V ∧ 𝐵 ∈ V), {{𝐶}, {𝐶, 𝐵}}, ∅)
8	5, 6, 7	3eqtr4g 2796	1 ⊢ (𝐴 = 𝐵 → ⟨𝐶, 𝐴⟩ = ⟨𝐶, 𝐵⟩)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1541   ∈ wcel 2113  Vcvv 3440  ∅c0 4285  ifcif 4479  {csn 4580  {cpr 4582  ⟨cop 4586

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587

This theorem is referenced by:  opeq12  4831  opeq2i  4833  opeq2d  4836  oteq2  4839  oteq3  4840  breq2  5102  cbvopab2  5174  cbvopab2v  5177  opthg  5425  eqvinop  5435  opelopabsb  5478  dfid3  5522  opelxp  5660  relopabi  5771  opabid2  5777  elrn2g  5839  opeldmd  5855  opeldm  5856  iss  5994  elidinxp  6003  dmsnopg  6171  reuop  6251  funopg  6526  f1osng  6816  f1oprswap  6819  tz6.12f  6859  fvn0ssdmfun  7019  fsn  7080  fsng  7082  fprg  7100  fprb  7140  oveq2  7366  cbvoprab2  7446  cbvoprab3v  7450  ovg  7523  elxp4  7864  elxp5  7865  opabex3d  7909  opabex3rd  7910  opabex3  7911  op1stg  7945  op2ndg  7946  op1steq  7977  dfoprab4f  8000  fsplit  8059  xpord2pred  8087  seqomlem2  8382  omeu  8512  oeeui  8530  ralxpmap  8834  elixpsn  8875  ixpsnf1o  8876  mapsnend  8973  xpsnen  8989  xpassen  8999  xpf1o  9067  unxpdomlem1  9156  djulcl  9822  djurcl  9823  djur  9831  djuss  9832  djuun  9838  1stinl  9839  2ndinl  9840  1stinr  9841  2ndinr  9842  axdc4lem  10365  nqereu  10840  mulcanenq  10871  elreal  11042  ax1rid  11072  fseq1p1m1  13514  pfxval  14597  swrdccatin1  14648  swrdccat3blem  14662  wrdlen2  14867  ruclem1  16156  imasaddfnlem  17449  imasvscafn  17458  catidex  17597  catpropd  17632  funcsetcestrclem1  18077  symg2bas  19322  efgi  19648  gsumcom2  19904  pzriprnglem3  21438  pzriprnglem10  21445  mat1rhmval  22423  mat1ric  22431  txkgen  23596  cnmpt21  23615  xkoinjcn  23631  txconn  23633  xpstopnlem1  23753  qustgplem  24065  metustid  24498  axlowdim2  29033  axlowdim  29034  axcontlem2  29038  axcontlem3  29039  axcontlem4  29040  axcontlem9  29045  axcontlem10  29046  axcontlem11  29047  cusgrexg  29517  rgrusgrprc  29663  2clwwlk2clwwlk  30425  isnvlem  30685  br8d  32686  gsumhashmul  33150  prsdm  34071  eulerpartlemgvv  34533  reprsuc  34772  bnj941  34928  bnj944  35094  fineqvrep  35270  cvmlift2lem1  35496  cvmlift2lem12  35508  goel  35541  gonafv  35544  satf0op  35571  sat1el2xp  35573  fmla0xp  35577  sategoelfvb  35613  br8  35950  br6  35951  br4  35952  dfrn5  35968  elima4  35970  pprodss4v  36076  brimg  36129  brapply  36130  lemsuccf  36133  brrestrict  36143  dfrdg4  36145  cgrtriv  36196  brofs  36199  segconeu  36205  btwntriv2  36206  transportprops  36228  brifs  36237  ifscgr  36238  brcgr3  36240  cgrxfr  36249  brcolinear2  36252  colineardim1  36255  brfs  36273  idinside  36278  btwnconn1lem7  36287  btwnconn1lem11  36291  btwnconn1lem12  36292  btwnconn1lem14  36294  brsegle  36302  seglerflx  36306  seglemin  36307  segleantisym  36309  btwnsegle  36311  outsideofeu  36325  outsidele  36326  linedegen  36337  fvline  36338  cbvoprab2vw  36432  cbvoprab23vw  36434  cbvopab2davw  36459  cbvoprab2davw  36466  finxpreclem6  37601  finxpsuclem  37602  curfv  37801  poimirlem4  37825  poimirlem26  37847  isdivrngo  38151  drngoi  38152  iss2  38537  dibelval3  41407  diblsmopel  41431  dihjatcclem4  41681  frlmsnic  42795  dfhe3  44016  dffrege115  44219  dropab2  44688  relopabVD  45141  projf1o  45441  sge0xp  46673  hoidmv1le  46838  fsetsniunop  47295  fsetsnf  47297  fsetsnf1  47298  fsetsnfo  47299  ichnreuop  47718  ichreuopeq  47719  reuopreuprim  47772  gpgprismgriedgdmss  48298  gpgvtx0  48299  gpgvtx1  48300  gpgedgvtx0  48307  gpgedgvtx1  48308  gpgedgiov  48311  gpgedg2ov  48312  gpgedg2iv  48313  gpg3kgrtriexlem6  48334  gpgprismgr4cycllem3  48343  pgnbgreunbgrlem1  48359  pgnbgreunbgrlem2  48363  pgnbgreunbgrlem4  48365  pgnbgreunbgrlem5lem1  48366  pgnbgreunbgrlem5lem2  48367  pgnbgreunbgrlem5lem3  48368  pgnbgreunbgrlem5  48369  gpg5edgnedg  48376  0aryfvalel  48880  1arymaptf1  48888  2arymaptf1  48899  prelrrx2b  48960  rrx2xpref1o  48964  rrx2plordisom  48969  sectpropdlem  49281  ssccatid  49317  isthincd2lem2  49680