Theorem opeq2 4840

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1569   ∈ wcel 2144  Vcvv 3450  ∅c0 4277  ifcif 4481  {csn 4584  {cpr 4586  ⟨cop 4834

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-ss 3897  df-dif 4046  df-un 4150  df-nul 4278  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835

This theorem is used by:  opeq12  4841  opeq2i  4843  opeq2d  4846  oteq2  4860  oteq3  4861  breq2  5106  cbvopab2  5180  cbvopab2v  5183  opthg  5446  eqvinop  5456  opelopabsb  5504  dfid3  5549  opelxp  5687  relopabi  5801  opabid2  5807  elrn2g  5873  opeldmd  5889  opeldm  5890  iss  6029  elidinxp  6038  dmsnopg  6217  reuop  6299  funopg  6579  f1osng  6872  f1oprswap  6875  tz6.12f  6915  fvn0ssdmfun  7079  fsn  7141  fsng  7143  fprg  7164  fprb  7203  oveq2  7432  cbvoprab2  7512  cbvoprab3v  7516  ovg  7589  elxp4  7938  elxp5  7939  opabex3d  7981  opabex3rd  7982  opabex3  7983  op1stg  8017  op2ndg  8018  op1steq  8049  dfoprab4f  8072  fsplit  8135  xpord2pred  8169  seqomlem2  8469  omeu  8601  oeeui  8619  curfv  8900  ralxpmap  8932  elixpsn  8973  ixpsnf1o  8974  mapsnend  9072  xpsnen  9088  xpassen  9098  xpf1o  9166  unxpdomlem1  9255  djulcl  9998  djurcl  9999  djur  10007  djuss  10008  djuun  10014  1stinl  10015  2ndinl  10016  1stinr  10017  2ndinr  10018  axdc4lem  10540  nqereu  11021  mulcanenq  11052  elreal  11223  ax1rid  11253  fseq1p1m1  13739  pfxval  14831  swrdccatin1  14882  swrdccat3blem  14896  wrdlen2  15104  ruclem1  16408  imasaddfnlem  17709  imasvscafn  17718  catidex  17857  catpropd  17892  funcsetcestrclem1  18337  degenmgm  19146  degenmgm2nfun  19148  degenmgm2  19149  symg2bas  19616  efgi  19942  gsumcom2  20198  pzriprnglem3  21798  pzriprnglem10  21805  mat1rhmval  22803  mat1ric  22811  txkgen  23980  cnmpt21  23999  xkoinjcn  24015  txconn  24017  xpstopnlem1  24137  qustgplem  24449  metustid  24882  angmgmval  29403  axlowdim2  29547  axlowdim  29548  axcontlem2  29552  axcontlem3  29553  axcontlem4  29554  axcontlem9  29559  axcontlem10  29560  axcontlem11  29561  cusgrexg  30034  rgrusgrprc  30179  2clwwlk2clwwlk  30960  isnvlem  31221  br8d  33253  gsumhashmul  33678  prsdm  34596  eulerpartlemgvv  35058  reprsuc  35294  bnj941  35453  bnj944  35618  omeueq  35773  soinfdom  35774  fineqvrep  35850  j00smo  35956  maxssj0  35957  j0le  35970  k3n0j0lt  35971  jltaleph  35977  cvmlift2lem1  36185  cvmlift2lem12  36197  goel  36230  gonafv  36233  satf0op  36260  sat1el2xp  36262  fmla0xp  36266  sategoelfvb  36302  br8  36645  br6  36646  br4  36647  dfrn5  36662  elima4  36664  pprodss4v  36770  brimg  36823  brapply  36824  lemsuccf  36827  brrestrict  36837  dfrdg4  36839  cgrtriv  36891  brofs  36894  segconeu  36900  btwntriv2  36901  transportprops  36923  brifs  36932  ifscgr  36933  brcgr3  36935  cgrxfr  36944  brcolinear2  36947  colineardim1  36950  brfs  36968  idinside  36973  btwnconn1lem7  36982  btwnconn1lem11  36986  btwnconn1lem12  36987  btwnconn1lem14  36989  brsegle  36997  seglerflx  37001  seglemin  37002  segleantisym  37004  btwnsegle  37006  outsideofeu  37020  outsidele  37021  linedegen  37032  fvline  37033  cbvoprab2vw  37151  cbvoprab23vw  37153  cbvopab2davw  37178  cbvoprab2davw  37185  finxpreclem6  38456  finxpsuclem  38457  poimirlem4  38679  poimirlem26  38701  isdivrngo  39021  drngoi  39022  iss2  39413  dibelval3  42341  diblsmopel  42365  dihjatcclem4  42615  frlmsnic  43741  dfhe3  44912  dffrege115  45115  dropab2  45567  relopabVD  46019  projf1o  46347  sge0xp  47575  hoidmv1le  47740  fsetsniunop  48255  fsetsnf  48257  fsetsnf1  48258  fsetsnfo  48259  ichnreuop  48690  ichreuopeq  48691  reuopreuprim  48744  gpgprismgriedgdmss  49286  gpgvtx0  49287  gpgvtx1  49288  gpgedgvtx0  49295  gpgedgvtx1  49296  gpgedgiov  49299  gpgedg2ov  49300  gpgedg2iv  49301  gpg3kgrtriexlem6  49322  gpgprismgr4cycllem3  49331  pgnbgreunbgrlem1  49347  pgnbgreunbgrlem2  49351  pgnbgreunbgrlem4  49353  pgnbgreunbgrlem5lem1  49354  pgnbgreunbgrlem5lem2  49355  pgnbgreunbgrlem5lem3  49356  pgnbgreunbgrlem5  49357  gpg5edgnedg  49364  0aryfvalel  49882  1arymaptf1  49890  2arymaptf1  49901  sectpropdlem  50286  ssccatid  50322  isthincd2lem2  50706  fuconuniqex2  50923