Theorem opeq2 4854

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 2821	. . . 4 ⊢ (𝐴 = 𝐵 → (𝐴 ∈ V ↔ 𝐵 ∈ V))
2	1	anbi2d 630	. . 3 ⊢ (𝐴 = 𝐵 → ((𝐶 ∈ V ∧ 𝐴 ∈ V) ↔ (𝐶 ∈ V ∧ 𝐵 ∈ V)))
3		preq2 4714	. . . 4 ⊢ (𝐴 = 𝐵 → {𝐶, 𝐴} = {𝐶, 𝐵})
4	3	preq2d 4720	. . 3 ⊢ (𝐴 = 𝐵 → {{𝐶}, {𝐶, 𝐴}} = {{𝐶}, {𝐶, 𝐵}})
5	2, 4	ifbieq1d 4530	. 2 ⊢ (𝐴 = 𝐵 → if((𝐶 ∈ V ∧ 𝐴 ∈ V), {{𝐶}, {𝐶, 𝐴}}, ∅) = if((𝐶 ∈ V ∧ 𝐵 ∈ V), {{𝐶}, {𝐶, 𝐵}}, ∅))
6		dfopif 4850	. 2 ⊢ ⟨𝐶, 𝐴⟩ = if((𝐶 ∈ V ∧ 𝐴 ∈ V), {{𝐶}, {𝐶, 𝐴}}, ∅)
7		dfopif 4850	. 2 ⊢ ⟨𝐶, 𝐵⟩ = if((𝐶 ∈ V ∧ 𝐵 ∈ V), {{𝐶}, {𝐶, 𝐵}}, ∅)
8	5, 6, 7	3eqtr4g 2794	1 ⊢ (𝐴 = 𝐵 → ⟨𝐶, 𝐴⟩ = ⟨𝐶, 𝐵⟩)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1539   ∈ wcel 2107  Vcvv 3463  ∅c0 4313  ifcif 4505  {csn 4606  {cpr 4608  ⟨cop 4612

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-sb 2064  df-clab 2713  df-cleq 2726  df-clel 2808  df-rab 3420  df-v 3465  df-dif 3934  df-un 3936  df-ss 3948  df-nul 4314  df-if 4506  df-sn 4607  df-pr 4609  df-op 4613

This theorem is referenced by:  opeq12  4855  opeq2i  4857  opeq2d  4860  oteq2  4863  oteq3  4864  breq2  5127  cbvopab2  5199  cbvopab2v  5203  opthg  5462  eqvinop  5472  opelopabsb  5515  dfid3  5561  opelxp  5701  relopabi  5812  opabid2  5818  elrn2g  5881  opeldmd  5897  opeldm  5898  iss  6033  elidinxp  6042  dmsnopg  6213  reuop  6293  funopg  6580  f1osng  6869  f1oprswap  6872  tz6.12f  6912  fvn0ssdmfun  7074  fsn  7135  fsng  7137  fprg  7155  fprb  7196  oveq2  7421  cbvoprab2  7503  cbvoprab3v  7507  ovg  7580  elxp4  7926  elxp5  7927  opabex3d  7972  opabex3rd  7973  opabex3  7974  op1stg  8008  op2ndg  8009  op1steq  8040  dfoprab4f  8063  fsplit  8124  xpord2pred  8152  seqomlem2  8473  omeu  8605  oeeui  8622  ralxpmap  8918  elixpsn  8959  ixpsnf1o  8960  mapsnend  9058  xpsnen  9077  xpassen  9088  xpf1o  9161  unxpdomlem1  9268  djulcl  9932  djurcl  9933  djur  9941  djuss  9942  djuun  9948  1stinl  9949  2ndinl  9950  1stinr  9951  2ndinr  9952  axdc4lem  10477  nqereu  10951  mulcanenq  10982  elreal  11153  ax1rid  11183  fseq1p1m1  13620  pfxval  14693  swrdccatin1  14745  swrdccat3blem  14759  wrdlen2  14965  ruclem1  16249  imasaddfnlem  17544  imasvscafn  17553  catidex  17688  catpropd  17723  funcsetcestrclem1  18169  symg2bas  19378  efgi  19705  gsumcom2  19961  pzriprnglem3  21456  pzriprnglem10  21463  mat1rhmval  22433  mat1ric  22441  txkgen  23606  cnmpt21  23625  xkoinjcn  23641  txconn  23643  xpstopnlem1  23763  qustgplem  24075  metustid  24511  axlowdim2  28905  axlowdim  28906  axcontlem2  28910  axcontlem3  28911  axcontlem4  28912  axcontlem9  28917  axcontlem10  28918  axcontlem11  28919  cusgrexg  29389  rgrusgrprc  29535  2clwwlk2clwwlk  30297  isnvlem  30557  br8d  32557  gsumhashmul  33003  prsdm  33872  eulerpartlemgvv  34337  reprsuc  34589  bnj941  34745  bnj944  34911  fineqvrep  35068  cvmlift2lem1  35266  cvmlift2lem12  35278  goel  35311  gonafv  35314  satf0op  35341  sat1el2xp  35343  fmla0xp  35347  sategoelfvb  35383  br8  35715  br6  35716  br4  35717  dfrn5  35733  elima4  35735  pprodss4v  35844  brimg  35897  brapply  35898  brsuccf  35901  brrestrict  35909  dfrdg4  35911  cgrtriv  35962  brofs  35965  segconeu  35971  btwntriv2  35972  transportprops  35994  brifs  36003  ifscgr  36004  brcgr3  36006  cgrxfr  36015  brcolinear2  36018  colineardim1  36021  brfs  36039  idinside  36044  btwnconn1lem7  36053  btwnconn1lem11  36057  btwnconn1lem12  36058  btwnconn1lem14  36060  brsegle  36068  seglerflx  36072  seglemin  36073  segleantisym  36075  btwnsegle  36077  outsideofeu  36091  outsidele  36092  linedegen  36103  fvline  36104  cbvoprab2vw  36198  cbvoprab23vw  36200  cbvopab2davw  36225  cbvoprab2davw  36232  finxpreclem6  37356  finxpsuclem  37357  curfv  37566  poimirlem4  37590  poimirlem26  37612  isdivrngo  37916  drngoi  37917  iss2  38304  dibelval3  41108  diblsmopel  41132  dihjatcclem4  41382  frlmsnic  42513  dfhe3  43750  dffrege115  43953  dropab2  44424  relopabVD  44878  projf1o  45159  sge0xp  46401  hoidmv1le  46566  fsetsniunop  47019  fsetsnf  47021  fsetsnf1  47022  fsetsnfo  47023  ichnreuop  47417  ichreuopeq  47418  reuopreuprim  47471  gpgvtx0  47966  gpgvtx1  47967  gpgedgvtx0  47977  gpgedgvtx1  47978  gpg3kgrtriexlem6  48002  0aryfvalel  48513  1arymaptf1  48521  2arymaptf1  48532  prelrrx2b  48593  rrx2xpref1o  48597  rrx2plordisom  48602  isthincd2lem2  49062