Theorem opeq2 4817

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 631	. . 3 ⊢ (𝐴 = 𝐵 → ((𝐶 ∈ V ∧ 𝐴 ∈ V) ↔ (𝐶 ∈ V ∧ 𝐵 ∈ V)))
3		preq2 4678	. . . 4 ⊢ (𝐴 = 𝐵 → {𝐶, 𝐴} = {𝐶, 𝐵})
4	3	preq2d 4684	. . 3 ⊢ (𝐴 = 𝐵 → {{𝐶}, {𝐶, 𝐴}} = {{𝐶}, {𝐶, 𝐵}})
5	2, 4	ifbieq1d 4491	. 2 ⊢ (𝐴 = 𝐵 → if((𝐶 ∈ V ∧ 𝐴 ∈ V), {{𝐶}, {𝐶, 𝐴}}, ∅) = if((𝐶 ∈ V ∧ 𝐵 ∈ V), {{𝐶}, {𝐶, 𝐵}}, ∅))
6		dfopif 4813	. 2 ⊢ ⟨𝐶, 𝐴⟩ = if((𝐶 ∈ V ∧ 𝐴 ∈ V), {{𝐶}, {𝐶, 𝐴}}, ∅)
7		dfopif 4813	. 2 ⊢ ⟨𝐶, 𝐵⟩ = if((𝐶 ∈ V ∧ 𝐵 ∈ V), {{𝐶}, {𝐶, 𝐵}}, ∅)
8	5, 6, 7	3eqtr4g 2796	1 ⊢ (𝐴 = 𝐵 → ⟨𝐶, 𝐴⟩ = ⟨𝐶, 𝐵⟩)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1542   ∈ wcel 2114  Vcvv 3429  ∅c0 4273  ifcif 4466  {csn 4567  {cpr 4569  ⟨cop 4573

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574

This theorem is referenced by:  opeq12  4818  opeq2i  4820  opeq2d  4823  oteq2  4826  oteq3  4827  breq2  5089  cbvopab2  5161  cbvopab2v  5164  opthg  5430  eqvinop  5440  opelopabsb  5485  dfid3  5529  opelxp  5667  relopabi  5778  opabid2  5784  elrn2g  5845  opeldmd  5861  opeldm  5862  iss  6000  elidinxp  6009  dmsnopg  6177  reuop  6257  funopg  6532  f1osng  6822  f1oprswap  6825  tz6.12f  6865  fvn0ssdmfun  7026  fsn  7088  fsng  7090  fprg  7109  fprb  7149  oveq2  7375  cbvoprab2  7455  cbvoprab3v  7459  ovg  7532  elxp4  7873  elxp5  7874  opabex3d  7918  opabex3rd  7919  opabex3  7920  op1stg  7954  op2ndg  7955  op1steq  7986  dfoprab4f  8009  fsplit  8067  xpord2pred  8095  seqomlem2  8390  omeu  8520  oeeui  8538  ralxpmap  8844  elixpsn  8885  ixpsnf1o  8886  mapsnend  8983  xpsnen  8999  xpassen  9009  xpf1o  9077  unxpdomlem1  9166  djulcl  9834  djurcl  9835  djur  9843  djuss  9844  djuun  9850  1stinl  9851  2ndinl  9852  1stinr  9853  2ndinr  9854  axdc4lem  10377  nqereu  10852  mulcanenq  10883  elreal  11054  ax1rid  11084  fseq1p1m1  13552  pfxval  14636  swrdccatin1  14687  swrdccat3blem  14701  wrdlen2  14906  ruclem1  16198  imasaddfnlem  17492  imasvscafn  17501  catidex  17640  catpropd  17675  funcsetcestrclem1  18120  symg2bas  19368  efgi  19694  gsumcom2  19950  pzriprnglem3  21463  pzriprnglem10  21470  mat1rhmval  22444  mat1ric  22452  txkgen  23617  cnmpt21  23636  xkoinjcn  23652  txconn  23654  xpstopnlem1  23774  qustgplem  24086  metustid  24519  axlowdim2  29029  axlowdim  29030  axcontlem2  29034  axcontlem3  29035  axcontlem4  29036  axcontlem9  29041  axcontlem10  29042  axcontlem11  29043  cusgrexg  29513  rgrusgrprc  29658  2clwwlk2clwwlk  30420  isnvlem  30681  br8d  32681  gsumhashmul  33128  prsdm  34058  eulerpartlemgvv  34520  reprsuc  34759  bnj941  34915  bnj944  35080  fineqvrep  35258  cvmlift2lem1  35484  cvmlift2lem12  35496  goel  35529  gonafv  35532  satf0op  35559  sat1el2xp  35561  fmla0xp  35565  sategoelfvb  35601  br8  35938  br6  35939  br4  35940  dfrn5  35956  elima4  35958  pprodss4v  36064  brimg  36117  brapply  36118  lemsuccf  36121  brrestrict  36131  dfrdg4  36133  cgrtriv  36184  brofs  36187  segconeu  36193  btwntriv2  36194  transportprops  36216  brifs  36225  ifscgr  36226  brcgr3  36228  cgrxfr  36237  brcolinear2  36240  colineardim1  36243  brfs  36261  idinside  36266  btwnconn1lem7  36275  btwnconn1lem11  36279  btwnconn1lem12  36280  btwnconn1lem14  36282  brsegle  36290  seglerflx  36294  seglemin  36295  segleantisym  36297  btwnsegle  36299  outsideofeu  36313  outsidele  36314  linedegen  36325  fvline  36326  cbvoprab2vw  36420  cbvoprab23vw  36422  cbvopab2davw  36447  cbvoprab2davw  36454  finxpreclem6  37712  finxpsuclem  37713  curfv  37921  poimirlem4  37945  poimirlem26  37967  isdivrngo  38271  drngoi  38272  iss2  38665  dibelval3  41593  diblsmopel  41617  dihjatcclem4  41867  frlmsnic  42985  dfhe3  44202  dffrege115  44405  dropab2  44874  relopabVD  45327  projf1o  45626  sge0xp  46857  hoidmv1le  47022  fsetsniunop  47497  fsetsnf  47499  fsetsnf1  47500  fsetsnfo  47501  ichnreuop  47932  ichreuopeq  47933  reuopreuprim  47986  gpgprismgriedgdmss  48528  gpgvtx0  48529  gpgvtx1  48530  gpgedgvtx0  48537  gpgedgvtx1  48538  gpgedgiov  48541  gpgedg2ov  48542  gpgedg2iv  48543  gpg3kgrtriexlem6  48564  gpgprismgr4cycllem3  48573  pgnbgreunbgrlem1  48589  pgnbgreunbgrlem2  48593  pgnbgreunbgrlem4  48595  pgnbgreunbgrlem5lem1  48596  pgnbgreunbgrlem5lem2  48597  pgnbgreunbgrlem5lem3  48598  pgnbgreunbgrlem5  48599  gpg5edgnedg  48606  0aryfvalel  49110  1arymaptf1  49118  2arymaptf1  49129  prelrrx2b  49190  rrx2xpref1o  49194  rrx2plordisom  49199  sectpropdlem  49511  ssccatid  49547  isthincd2lem2  49910