Theorem opeq2 4826

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 2844	. . . 4 ⊢ (𝐴 = 𝐵 → (𝐴 ∈ V ↔ 𝐵 ∈ V))
2	1	anbi2d 638	. . 3 ⊢ (𝐴 = 𝐵 → ((𝐶 ∈ V ∧ 𝐴 ∈ V) ↔ (𝐶 ∈ V ∧ 𝐵 ∈ V)))
3		preq2 4687	. . . 4 ⊢ (𝐴 = 𝐵 → {𝐶, 𝐴} = {𝐶, 𝐵})
4	3	preq2d 4693	. . 3 ⊢ (𝐴 = 𝐵 → {{𝐶}, {𝐶, 𝐴}} = {{𝐶}, {𝐶, 𝐵}})
5	2, 4	ifbieq1d 4499	. 2 ⊢ (𝐴 = 𝐵 → if((𝐶 ∈ V ∧ 𝐴 ∈ V), {{𝐶}, {𝐶, 𝐴}}, ∅) = if((𝐶 ∈ V ∧ 𝐵 ∈ V), {{𝐶}, {𝐶, 𝐵}}, ∅))
6		dfopif 4822	. 2 ⊢ ⟨𝐶, 𝐴⟩ = if((𝐶 ∈ V ∧ 𝐴 ∈ V), {{𝐶}, {𝐶, 𝐴}}, ∅)
7		dfopif 4822	. 2 ⊢ ⟨𝐶, 𝐵⟩ = if((𝐶 ∈ V ∧ 𝐵 ∈ V), {{𝐶}, {𝐶, 𝐵}}, ∅)
8	5, 6, 7	3eqtr4g 2816	1 ⊢ (𝐴 = 𝐵 → ⟨𝐶, 𝐴⟩ = ⟨𝐶, 𝐵⟩)

Syntax hints:   → wi 4   ∧ wa 398   = wceq 1554   ∈ wcel 2136  Vcvv 3448  ∅c0 4280  ifcif 4474  {csn 4576  {cpr 4578  ⟨cop 4582

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1809  ax-4 1823  ax-5 1924  ax-6 1981  ax-7 2022  ax-8 2138  ax-9 2146  ax-ext 2728

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 857  df-3an 1097  df-tru 1557  df-fal 1567  df-ex 1794  df-sb 2085  df-clab 2735  df-cleq 2748  df-clel 2831  df-rab 3409  df-v 3450  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4281  df-if 4475  df-sn 4577  df-pr 4579  df-op 4583

This theorem is referenced by:  opeq12  4827  opeq2i  4829  opeq2d  4832  oteq2  4835  oteq3  4836  breq2  5098  cbvopab2  5170  cbvopab2v  5173  opthg  5439  eqvinop  5449  opelopabsb  5494  dfid3  5538  opelxp  5676  relopabi  5788  opabid2  5794  elrn2g  5859  opeldmd  5875  opeldm  5876  iss  6014  elidinxp  6023  dmsnopg  6189  reuop  6269  funopg  6544  f1osng  6838  f1oprswap  6841  tz6.12f  6881  fvn0ssdmfun  7044  fsn  7106  fsng  7108  fprg  7127  fprb  7167  oveq2  7393  cbvoprab2  7473  cbvoprab3v  7477  ovg  7550  elxp4  7892  elxp5  7893  opabex3d  7935  opabex3rd  7936  opabex3  7937  op1stg  7971  op2ndg  7972  op1steq  8003  dfoprab4f  8026  fsplit  8084  xpord2pred  8113  seqomlem2  8410  omeu  8542  oeeui  8560  ralxpmap  8867  elixpsn  8908  ixpsnf1o  8909  mapsnend  9006  xpsnen  9022  xpassen  9032  xpf1o  9100  unxpdomlem1  9189  djulcl  9858  djurcl  9859  djur  9867  djuss  9868  djuun  9874  1stinl  9875  2ndinl  9876  1stinr  9877  2ndinr  9878  axdc4lem  10402  nqereu  10877  mulcanenq  10908  elreal  11079  ax1rid  11109  fseq1p1m1  13593  pfxval  14677  swrdccatin1  14728  swrdccat3blem  14742  wrdlen2  14947  ruclem1  16239  imasaddfnlem  17534  imasvscafn  17543  catidex  17682  catpropd  17717  funcsetcestrclem1  18162  symg2bas  19409  efgi  19735  gsumcom2  19991  pzriprnglem3  21508  pzriprnglem10  21515  mat1rhmval  22512  mat1ric  22520  txkgen  23685  cnmpt21  23704  xkoinjcn  23720  txconn  23722  xpstopnlem1  23842  qustgplem  24154  metustid  24587  axlowdim2  29100  axlowdim  29101  axcontlem2  29105  axcontlem3  29106  axcontlem4  29107  axcontlem9  29112  axcontlem10  29113  axcontlem11  29114  cusgrexg  29584  rgrusgrprc  29729  2clwwlk2clwwlk  30491  isnvlem  30752  br8d  32753  gsumhashmul  33201  prsdm  34165  eulerpartlemgvv  34627  reprsuc  34866  bnj941  35025  bnj944  35190  fineqvrep  35365  cvmlift2lem1  35600  cvmlift2lem12  35612  goel  35645  gonafv  35648  satf0op  35675  sat1el2xp  35677  fmla0xp  35681  sategoelfvb  35717  br8  36054  br6  36055  br4  36056  dfrn5  36072  elima4  36074  pprodss4v  36180  brimg  36233  brapply  36234  lemsuccf  36237  brrestrict  36247  dfrdg4  36249  cgrtriv  36300  brofs  36303  segconeu  36309  btwntriv2  36310  transportprops  36332  brifs  36341  ifscgr  36342  brcgr3  36344  cgrxfr  36353  brcolinear2  36356  colineardim1  36359  brfs  36377  idinside  36382  btwnconn1lem7  36391  btwnconn1lem11  36395  btwnconn1lem12  36396  btwnconn1lem14  36398  brsegle  36406  seglerflx  36410  seglemin  36411  segleantisym  36413  btwnsegle  36415  outsideofeu  36429  outsidele  36430  linedegen  36441  fvline  36442  cbvoprab2vw  36546  cbvoprab23vw  36548  cbvopab2davw  36573  cbvoprab2davw  36580  finxpreclem6  37838  finxpsuclem  37839  curfv  38047  poimirlem4  38071  poimirlem26  38093  isdivrngo  38397  drngoi  38398  iss2  38791  dibelval3  41719  diblsmopel  41743  dihjatcclem4  41993  frlmsnic  43106  dfhe3  44299  dffrege115  44502  dropab2  44971  relopabVD  45424  projf1o  45722  sge0xp  46951  hoidmv1le  47116  fsetsniunop  47591  fsetsnf  47593  fsetsnf1  47594  fsetsnfo  47595  ichnreuop  48026  ichreuopeq  48027  reuopreuprim  48080  gpgprismgriedgdmss  48622  gpgvtx0  48623  gpgvtx1  48624  gpgedgvtx0  48631  gpgedgvtx1  48632  gpgedgiov  48635  gpgedg2ov  48636  gpgedg2iv  48637  gpg3kgrtriexlem6  48658  gpgprismgr4cycllem3  48667  pgnbgreunbgrlem1  48683  pgnbgreunbgrlem2  48687  pgnbgreunbgrlem4  48689  pgnbgreunbgrlem5lem1  48690  pgnbgreunbgrlem5lem2  48691  pgnbgreunbgrlem5lem3  48692  pgnbgreunbgrlem5  48693  gpg5edgnedg  48700  0aryfvalel  49204  1arymaptf1  49212  2arymaptf1  49223  prelrrx2b  49284  rrx2xpref1o  49288  rrx2plordisom  49293  sectpropdlem  49605  ssccatid  49641  isthincd2lem2  50004