Theorem opeq2 4856

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 4716	. . . 4 ⊢ (𝐴 = 𝐵 → {𝐶, 𝐴} = {𝐶, 𝐵})
4	3	preq2d 4722	. . 3 ⊢ (𝐴 = 𝐵 → {{𝐶}, {𝐶, 𝐴}} = {{𝐶}, {𝐶, 𝐵}})
5	2, 4	ifbieq1d 4532	. 2 ⊢ (𝐴 = 𝐵 → if((𝐶 ∈ V ∧ 𝐴 ∈ V), {{𝐶}, {𝐶, 𝐴}}, ∅) = if((𝐶 ∈ V ∧ 𝐵 ∈ V), {{𝐶}, {𝐶, 𝐵}}, ∅))
6		dfopif 4852	. 2 ⊢ ⟨𝐶, 𝐴⟩ = if((𝐶 ∈ V ∧ 𝐴 ∈ V), {{𝐶}, {𝐶, 𝐴}}, ∅)
7		dfopif 4852	. 2 ⊢ ⟨𝐶, 𝐵⟩ = if((𝐶 ∈ V ∧ 𝐵 ∈ V), {{𝐶}, {𝐶, 𝐵}}, ∅)
8	5, 6, 7	3eqtr4g 2794	1 ⊢ (𝐴 = 𝐵 → ⟨𝐶, 𝐴⟩ = ⟨𝐶, 𝐵⟩)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1539   ∈ wcel 2107  Vcvv 3464  ∅c0 4315  ifcif 4507  {csn 4608  {cpr 4610  ⟨cop 4614

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 3421  df-v 3466  df-dif 3936  df-un 3938  df-ss 3950  df-nul 4316  df-if 4508  df-sn 4609  df-pr 4611  df-op 4615

This theorem is referenced by:  opeq12  4857  opeq2i  4859  opeq2d  4862  oteq2  4865  oteq3  4866  breq2  5129  cbvopab2  5201  cbvopab2v  5205  opthg  5464  eqvinop  5474  opelopabsb  5517  dfid3  5563  opelxp  5703  relopabi  5814  opabid2  5820  elrn2g  5883  opeldmd  5899  opeldm  5900  iss  6035  elidinxp  6044  dmsnopg  6215  reuop  6295  funopg  6581  f1osng  6870  f1oprswap  6873  tz6.12f  6913  fvn0ssdmfun  7075  fsn  7136  fsng  7138  fprg  7156  fprb  7197  oveq2  7422  cbvoprab2  7504  cbvoprab3v  7508  ovg  7581  elxp4  7927  elxp5  7928  opabex3d  7973  opabex3rd  7974  opabex3  7975  op1stg  8009  op2ndg  8010  op1steq  8041  dfoprab4f  8064  fsplit  8125  xpord2pred  8153  seqomlem2  8474  omeu  8606  oeeui  8623  ralxpmap  8919  elixpsn  8960  ixpsnf1o  8961  mapsnend  9059  xpsnen  9078  xpassen  9089  xpf1o  9162  unxpdomlem1  9269  djulcl  9933  djurcl  9934  djur  9942  djuss  9943  djuun  9949  1stinl  9950  2ndinl  9951  1stinr  9952  2ndinr  9953  axdc4lem  10478  nqereu  10952  mulcanenq  10983  elreal  11154  ax1rid  11184  fseq1p1m1  13621  pfxval  14694  swrdccatin1  14746  swrdccat3blem  14760  wrdlen2  14966  ruclem1  16250  imasaddfnlem  17549  imasvscafn  17558  catidex  17693  catpropd  17728  funcsetcestrclem1  18174  symg2bas  19383  efgi  19710  gsumcom2  19966  pzriprnglem3  21461  pzriprnglem10  21468  mat1rhmval  22452  mat1ric  22460  txkgen  23625  cnmpt21  23644  xkoinjcn  23660  txconn  23662  xpstopnlem1  23782  qustgplem  24094  metustid  24530  axlowdim2  28924  axlowdim  28925  axcontlem2  28929  axcontlem3  28930  axcontlem4  28931  axcontlem9  28936  axcontlem10  28937  axcontlem11  28938  cusgrexg  29408  rgrusgrprc  29554  2clwwlk2clwwlk  30316  isnvlem  30576  br8d  32569  gsumhashmul  33010  prsdm  33854  eulerpartlemgvv  34319  reprsuc  34571  bnj941  34727  bnj944  34893  fineqvrep  35050  cvmlift2lem1  35248  cvmlift2lem12  35260  goel  35293  gonafv  35296  satf0op  35323  sat1el2xp  35325  fmla0xp  35329  sategoelfvb  35365  br8  35697  br6  35698  br4  35699  dfrn5  35715  elima4  35717  pprodss4v  35826  brimg  35879  brapply  35880  brsuccf  35883  brrestrict  35891  dfrdg4  35893  cgrtriv  35944  brofs  35947  segconeu  35953  btwntriv2  35954  transportprops  35976  brifs  35985  ifscgr  35986  brcgr3  35988  cgrxfr  35997  brcolinear2  36000  colineardim1  36003  brfs  36021  idinside  36026  btwnconn1lem7  36035  btwnconn1lem11  36039  btwnconn1lem12  36040  btwnconn1lem14  36042  brsegle  36050  seglerflx  36054  seglemin  36055  segleantisym  36057  btwnsegle  36059  outsideofeu  36073  outsidele  36074  linedegen  36085  fvline  36086  cbvoprab2vw  36180  cbvoprab23vw  36182  cbvopab2davw  36207  cbvoprab2davw  36214  finxpreclem6  37338  finxpsuclem  37339  curfv  37548  poimirlem4  37572  poimirlem26  37594  isdivrngo  37898  drngoi  37899  iss2  38286  dibelval3  41090  diblsmopel  41114  dihjatcclem4  41364  frlmsnic  42495  dfhe3  43733  dffrege115  43936  dropab2  44412  relopabVD  44866  projf1o  45147  sge0xp  46389  hoidmv1le  46554  fsetsniunop  47007  fsetsnf  47009  fsetsnf1  47010  fsetsnfo  47011  ichnreuop  47405  ichreuopeq  47406  reuopreuprim  47459  gpgvtx0  47954  gpgvtx1  47955  gpgedgvtx0  47965  gpgedgvtx1  47966  gpg3kgrtriexlem6  47990  0aryfvalel  48501  1arymaptf1  48509  2arymaptf1  48520  prelrrx2b  48581  rrx2xpref1o  48585  rrx2plordisom  48590  isthincd2lem2  49050