Theorem opeq2 4855

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2109  Vcvv 3464  ∅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 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2715  df-cleq 2728  df-clel 2810  df-rab 3421  df-v 3466  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  4856  opeq2i  4858  opeq2d  4861  oteq2  4864  oteq3  4865  breq2  5128  cbvopab2  5200  cbvopab2v  5204  opthg  5457  eqvinop  5467  opelopabsb  5510  dfid3  5556  opelxp  5695  relopabi  5806  opabid2  5812  elrn2g  5875  opeldmd  5891  opeldm  5892  iss  6027  elidinxp  6036  dmsnopg  6207  reuop  6287  funopg  6575  f1osng  6864  f1oprswap  6867  tz6.12f  6907  fvn0ssdmfun  7069  fsn  7130  fsng  7132  fprg  7150  fprb  7191  oveq2  7418  cbvoprab2  7500  cbvoprab3v  7504  ovg  7577  elxp4  7923  elxp5  7924  opabex3d  7969  opabex3rd  7970  opabex3  7971  op1stg  8005  op2ndg  8006  op1steq  8037  dfoprab4f  8060  fsplit  8121  xpord2pred  8149  seqomlem2  8470  omeu  8602  oeeui  8619  ralxpmap  8915  elixpsn  8956  ixpsnf1o  8957  mapsnend  9055  xpsnen  9074  xpassen  9085  xpf1o  9158  unxpdomlem1  9263  djulcl  9929  djurcl  9930  djur  9938  djuss  9939  djuun  9945  1stinl  9946  2ndinl  9947  1stinr  9948  2ndinr  9949  axdc4lem  10474  nqereu  10948  mulcanenq  10979  elreal  11150  ax1rid  11180  fseq1p1m1  13620  pfxval  14696  swrdccatin1  14748  swrdccat3blem  14762  wrdlen2  14968  ruclem1  16254  imasaddfnlem  17547  imasvscafn  17556  catidex  17691  catpropd  17726  funcsetcestrclem1  18171  symg2bas  19379  efgi  19705  gsumcom2  19961  pzriprnglem3  21449  pzriprnglem10  21456  mat1rhmval  22422  mat1ric  22430  txkgen  23595  cnmpt21  23614  xkoinjcn  23630  txconn  23632  xpstopnlem1  23752  qustgplem  24064  metustid  24498  axlowdim2  28944  axlowdim  28945  axcontlem2  28949  axcontlem3  28950  axcontlem4  28951  axcontlem9  28956  axcontlem10  28957  axcontlem11  28958  cusgrexg  29428  rgrusgrprc  29574  2clwwlk2clwwlk  30336  isnvlem  30596  br8d  32595  gsumhashmul  33060  prsdm  33950  eulerpartlemgvv  34413  reprsuc  34652  bnj941  34808  bnj944  34974  fineqvrep  35131  cvmlift2lem1  35329  cvmlift2lem12  35341  goel  35374  gonafv  35377  satf0op  35404  sat1el2xp  35406  fmla0xp  35410  sategoelfvb  35446  br8  35778  br6  35779  br4  35780  dfrn5  35796  elima4  35798  pprodss4v  35907  brimg  35960  brapply  35961  brsuccf  35964  brrestrict  35972  dfrdg4  35974  cgrtriv  36025  brofs  36028  segconeu  36034  btwntriv2  36035  transportprops  36057  brifs  36066  ifscgr  36067  brcgr3  36069  cgrxfr  36078  brcolinear2  36081  colineardim1  36084  brfs  36102  idinside  36107  btwnconn1lem7  36116  btwnconn1lem11  36120  btwnconn1lem12  36121  btwnconn1lem14  36123  brsegle  36131  seglerflx  36135  seglemin  36136  segleantisym  36138  btwnsegle  36140  outsideofeu  36154  outsidele  36155  linedegen  36166  fvline  36167  cbvoprab2vw  36261  cbvoprab23vw  36263  cbvopab2davw  36288  cbvoprab2davw  36295  finxpreclem6  37419  finxpsuclem  37420  curfv  37629  poimirlem4  37653  poimirlem26  37675  isdivrngo  37979  drngoi  37980  iss2  38367  dibelval3  41171  diblsmopel  41195  dihjatcclem4  41445  frlmsnic  42538  dfhe3  43774  dffrege115  43977  dropab2  44447  relopabVD  44900  projf1o  45201  sge0xp  46438  hoidmv1le  46603  fsetsniunop  47058  fsetsnf  47060  fsetsnf1  47061  fsetsnfo  47062  ichnreuop  47466  ichreuopeq  47467  reuopreuprim  47520  gpgprismgriedgdmss  48036  gpgvtx0  48037  gpgvtx1  48038  gpgedgvtx0  48045  gpgedgvtx1  48046  gpg3kgrtriexlem6  48070  gpgprismgr4cycllem3  48076  0aryfvalel  48594  1arymaptf1  48602  2arymaptf1  48613  prelrrx2b  48674  rrx2xpref1o  48678  rrx2plordisom  48683  sectpropdlem  48983  ssccatid  49019  isthincd2lem2  49301