Theorem opeq2 4841

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 2853	. . . 4 ⊢ (𝐴 = 𝐵 → (𝐴 ∈ V ↔ 𝐵 ∈ V))
2	1	anbi2d 642	. . 3 ⊢ (𝐴 = 𝐵 → ((𝐶 ∈ V ∧ 𝐴 ∈ V) ↔ (𝐶 ∈ V ∧ 𝐵 ∈ V)))
3		preq2 4702	. . . 4 ⊢ (𝐴 = 𝐵 → {𝐶, 𝐴} = {𝐶, 𝐵})
4	3	preq2d 4708	. . 3 ⊢ (𝐴 = 𝐵 → {{𝐶}, {𝐶, 𝐴}} = {{𝐶}, {𝐶, 𝐵}})
5	2, 4	ifbieq1d 4514	. 2 ⊢ (𝐴 = 𝐵 → if((𝐶 ∈ V ∧ 𝐴 ∈ V), {{𝐶}, {𝐶, 𝐴}}, ∅) = if((𝐶 ∈ V ∧ 𝐵 ∈ V), {{𝐶}, {𝐶, 𝐵}}, ∅))
6		dfopif 4837	. 2 ⊢ ⟨𝐶, 𝐴⟩ = if((𝐶 ∈ V ∧ 𝐴 ∈ V), {{𝐶}, {𝐶, 𝐴}}, ∅)
7		dfopif 4837	. 2 ⊢ ⟨𝐶, 𝐵⟩ = if((𝐶 ∈ V ∧ 𝐵 ∈ V), {{𝐶}, {𝐶, 𝐵}}, ∅)
8	5, 6, 7	3eqtr4g 2825	1 ⊢ (𝐴 = 𝐵 → ⟨𝐶, 𝐴⟩ = ⟨𝐶, 𝐵⟩)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570   ∈ wcel 2146  Vcvv 3457  ∅c0 4286  ifcif 4489  {csn 4591  {cpr 4593  ⟨cop 4597

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-rab 3419  df-v 3459  df-dif 3909  df-un 3911  df-ss 3923  df-nul 4287  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598

This theorem is used by:  opeq12  4842  opeq2i  4844  opeq2d  4847  oteq2  4850  oteq3  4851  breq2  5115  cbvopab2  5189  cbvopab2v  5192  opthg  5461  eqvinop  5471  opelopabsb  5516  dfid3  5561  opelxp  5699  relopabi  5811  opabid2  5817  elrn2g  5882  opeldmd  5898  opeldm  5899  iss  6039  elidinxp  6048  dmsnopg  6216  reuop  6298  funopg  6574  f1osng  6867  f1oprswap  6870  tz6.12f  6910  fvn0ssdmfun  7073  fsn  7135  fsng  7137  fprg  7158  fprb  7198  oveq2  7427  cbvoprab2  7507  cbvoprab3v  7511  ovg  7584  elxp4  7925  elxp5  7926  opabex3d  7968  opabex3rd  7969  opabex3  7970  op1stg  8004  op2ndg  8005  op1steq  8036  dfoprab4f  8059  fsplit  8118  xpord2pred  8147  seqomlem2  8444  omeu  8576  oeeui  8594  ralxpmap  8900  elixpsn  8941  ixpsnf1o  8942  mapsnend  9040  xpsnen  9056  xpassen  9066  xpf1o  9134  unxpdomlem1  9223  djulcl  9912  djurcl  9913  djur  9921  djuss  9922  djuun  9928  1stinl  9929  2ndinl  9930  1stinr  9931  2ndinr  9932  axdc4lem  10454  nqereu  10929  mulcanenq  10960  elreal  11131  ax1rid  11161  fseq1p1m1  13643  pfxval  14733  swrdccatin1  14784  swrdccat3blem  14798  wrdlen2  15005  ruclem1  16309  imasaddfnlem  17604  imasvscafn  17613  catidex  17752  catpropd  17787  funcsetcestrclem1  18232  degenmgm  19037  degenmgm2nfun  19039  degenmgm2  19040  symg2bas  19507  efgi  19833  gsumcom2  20089  pzriprnglem3  21683  pzriprnglem10  21690  mat1rhmval  22686  mat1ric  22694  txkgen  23860  cnmpt21  23879  xkoinjcn  23895  txconn  23897  xpstopnlem1  24017  qustgplem  24329  metustid  24762  axlowdim2  29365  axlowdim  29366  axcontlem2  29370  axcontlem3  29371  axcontlem4  29372  axcontlem9  29377  axcontlem10  29378  axcontlem11  29379  cusgrexg  29852  rgrusgrprc  29997  2clwwlk2clwwlk  30772  isnvlem  31033  br8d  33024  gsumhashmul  33451  prsdm  34368  eulerpartlemgvv  34831  reprsuc  35067  bnj941  35226  bnj944  35391  fineqvrep  35584  cvmlift2lem1  35831  cvmlift2lem12  35843  goel  35876  gonafv  35879  satf0op  35906  sat1el2xp  35908  fmla0xp  35912  sategoelfvb  35948  br8  36285  br6  36286  br4  36287  dfrn5  36303  elima4  36305  pprodss4v  36411  brimg  36464  brapply  36465  lemsuccf  36468  brrestrict  36478  dfrdg4  36480  cgrtriv  36531  brofs  36534  segconeu  36540  btwntriv2  36541  transportprops  36563  brifs  36572  ifscgr  36573  brcgr3  36575  cgrxfr  36584  brcolinear2  36587  colineardim1  36590  brfs  36608  idinside  36613  btwnconn1lem7  36622  btwnconn1lem11  36626  btwnconn1lem12  36627  btwnconn1lem14  36629  brsegle  36637  seglerflx  36641  seglemin  36642  segleantisym  36644  btwnsegle  36646  outsideofeu  36660  outsidele  36661  linedegen  36672  fvline  36673  cbvoprab2vw  36807  cbvoprab23vw  36809  cbvopab2davw  36834  cbvoprab2davw  36841  finxpreclem6  38099  finxpsuclem  38100  curfv  38308  poimirlem4  38332  poimirlem26  38354  isdivrngo  38659  drngoi  38660  iss2  39051  dibelval3  41979  diblsmopel  42003  dihjatcclem4  42253  frlmsnic  43366  dfhe3  44559  dffrege115  44762  dropab2  45215  relopabVD  45667  projf1o  45972  sge0xp  47201  hoidmv1le  47366  fsetsniunop  47844  fsetsnf  47846  fsetsnf1  47847  fsetsnfo  47848  ichnreuop  48279  ichreuopeq  48280  reuopreuprim  48333  gpgprismgriedgdmss  48875  gpgvtx0  48876  gpgvtx1  48877  gpgedgvtx0  48884  gpgedgvtx1  48885  gpgedgiov  48888  gpgedg2ov  48889  gpgedg2iv  48890  gpg3kgrtriexlem6  48911  gpgprismgr4cycllem3  48920  pgnbgreunbgrlem1  48936  pgnbgreunbgrlem2  48940  pgnbgreunbgrlem4  48942  pgnbgreunbgrlem5lem1  48943  pgnbgreunbgrlem5lem2  48944  pgnbgreunbgrlem5lem3  48945  pgnbgreunbgrlem5  48946  gpg5edgnedg  48953  0aryfvalel  49471  1arymaptf1  49479  2arymaptf1  49490  prelrrx2b  49551  rrx2xpref1o  49555  rrx2plordisom  49560  sectpropdlem  49871  ssccatid  49907  isthincd2lem2  50270