Theorem opeq2 4879

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 2827	. . . 4 ⊢ (𝐴 = 𝐵 → (𝐴 ∈ V ↔ 𝐵 ∈ V))
2	1	anbi2d 630	. . 3 ⊢ (𝐴 = 𝐵 → ((𝐶 ∈ V ∧ 𝐴 ∈ V) ↔ (𝐶 ∈ V ∧ 𝐵 ∈ V)))
3		preq2 4739	. . . 4 ⊢ (𝐴 = 𝐵 → {𝐶, 𝐴} = {𝐶, 𝐵})
4	3	preq2d 4745	. . 3 ⊢ (𝐴 = 𝐵 → {{𝐶}, {𝐶, 𝐴}} = {{𝐶}, {𝐶, 𝐵}})
5	2, 4	ifbieq1d 4555	. 2 ⊢ (𝐴 = 𝐵 → if((𝐶 ∈ V ∧ 𝐴 ∈ V), {{𝐶}, {𝐶, 𝐴}}, ∅) = if((𝐶 ∈ V ∧ 𝐵 ∈ V), {{𝐶}, {𝐶, 𝐵}}, ∅))
6		dfopif 4875	. 2 ⊢ ⟨𝐶, 𝐴⟩ = if((𝐶 ∈ V ∧ 𝐴 ∈ V), {{𝐶}, {𝐶, 𝐴}}, ∅)
7		dfopif 4875	. 2 ⊢ ⟨𝐶, 𝐵⟩ = if((𝐶 ∈ V ∧ 𝐵 ∈ V), {{𝐶}, {𝐶, 𝐵}}, ∅)
8	5, 6, 7	3eqtr4g 2800	1 ⊢ (𝐴 = 𝐵 → ⟨𝐶, 𝐴⟩ = ⟨𝐶, 𝐵⟩)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1537   ∈ wcel 2106  Vcvv 3478  ∅c0 4339  ifcif 4531  {csn 4631  {cpr 4633  ⟨cop 4637

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-rab 3434  df-v 3480  df-dif 3966  df-un 3968  df-ss 3980  df-nul 4340  df-if 4532  df-sn 4632  df-pr 4634  df-op 4638

This theorem is referenced by:  opeq12  4880  opeq2i  4882  opeq2d  4885  oteq2  4888  oteq3  4889  breq2  5152  cbvopab2  5225  cbvopab2v  5229  opthg  5488  eqvinop  5498  opelopabsb  5540  dfid3  5586  opelxp  5725  relopabi  5835  opabid2  5841  elrn2g  5904  opeldmd  5920  opeldm  5921  iss  6055  elidinxp  6064  elimasngOLD  6111  dmsnopg  6235  reuop  6315  funopg  6602  f1osng  6890  f1oprswap  6893  tz6.12f  6933  fvn0ssdmfun  7094  fsn  7155  fsng  7157  fprg  7175  fprb  7214  oveq2  7439  cbvoprab2  7521  cbvoprab3v  7525  ovg  7598  elxp4  7945  elxp5  7946  opabex3d  7989  opabex3rd  7990  opabex3  7991  op1stg  8025  op2ndg  8026  op1steq  8057  dfoprab4f  8080  fsplit  8141  xpord2pred  8169  seqomlem2  8490  omeu  8622  oeeui  8639  ralxpmap  8935  elixpsn  8976  ixpsnf1o  8977  mapsnend  9075  xpsnen  9094  xpassen  9105  xpf1o  9178  unxpdomlem1  9284  djulcl  9948  djurcl  9949  djur  9957  djuss  9958  djuun  9964  1stinl  9965  2ndinl  9966  1stinr  9967  2ndinr  9968  axdc4lem  10493  nqereu  10967  mulcanenq  10998  elreal  11169  ax1rid  11199  fseq1p1m1  13635  pfxval  14708  swrdccatin1  14760  swrdccat3blem  14774  wrdlen2  14980  ruclem1  16264  imasaddfnlem  17575  imasvscafn  17584  catidex  17719  catpropd  17754  funcsetcestrclem1  18210  symg2bas  19425  efgi  19752  gsumcom2  20008  pzriprnglem3  21512  pzriprnglem10  21519  mat1rhmval  22501  mat1ric  22509  txkgen  23676  cnmpt21  23695  xkoinjcn  23711  txconn  23713  xpstopnlem1  23833  qustgplem  24145  metustid  24583  axlowdim2  28990  axlowdim  28991  axcontlem2  28995  axcontlem3  28996  axcontlem4  28997  axcontlem9  29002  axcontlem10  29003  axcontlem11  29004  cusgrexg  29476  rgrusgrprc  29622  2clwwlk2clwwlk  30379  isnvlem  30639  br8d  32630  gsumhashmul  33047  prsdm  33875  eulerpartlemgvv  34358  reprsuc  34609  bnj941  34765  bnj944  34931  fineqvrep  35088  cvmlift2lem1  35287  cvmlift2lem12  35299  goel  35332  gonafv  35335  satf0op  35362  sat1el2xp  35364  fmla0xp  35368  sategoelfvb  35404  br8  35736  br6  35737  br4  35738  dfrn5  35755  elima4  35757  pprodss4v  35866  brimg  35919  brapply  35920  brsuccf  35923  brrestrict  35931  dfrdg4  35933  cgrtriv  35984  brofs  35987  segconeu  35993  btwntriv2  35994  transportprops  36016  brifs  36025  ifscgr  36026  brcgr3  36028  cgrxfr  36037  brcolinear2  36040  colineardim1  36043  brfs  36061  idinside  36066  btwnconn1lem7  36075  btwnconn1lem11  36079  btwnconn1lem12  36080  btwnconn1lem14  36082  brsegle  36090  seglerflx  36094  seglemin  36095  segleantisym  36097  btwnsegle  36099  outsideofeu  36113  outsidele  36114  linedegen  36125  fvline  36126  cbvoprab2vw  36221  cbvoprab23vw  36223  cbvopab2davw  36248  cbvoprab2davw  36255  finxpreclem6  37379  finxpsuclem  37380  curfv  37587  poimirlem4  37611  poimirlem26  37633  isdivrngo  37937  drngoi  37938  iss2  38326  dibelval3  41130  diblsmopel  41154  dihjatcclem4  41404  frlmsnic  42527  dfhe3  43765  dffrege115  43968  dropab2  44444  relopabVD  44899  projf1o  45140  sge0xp  46385  hoidmv1le  46550  fsetsniunop  46999  fsetsnf  47001  fsetsnf1  47002  fsetsnfo  47003  ichnreuop  47397  ichreuopeq  47398  reuopreuprim  47451  gpgvtx0  47944  gpgvtx1  47945  gpgedgvtx0  47954  gpgedgvtx1  47955  0aryfvalel  48484  1arymaptf1  48492  2arymaptf1  48503  prelrrx2b  48564  rrx2xpref1o  48568  rrx2plordisom  48573  isthincd2lem2  48836