Theorem opeq2 4823

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 2819	. . . 4 ⊢ (𝐴 = 𝐵 → (𝐴 ∈ V ↔ 𝐵 ∈ V))
2	1	anbi2d 630	. . 3 ⊢ (𝐴 = 𝐵 → ((𝐶 ∈ V ∧ 𝐴 ∈ V) ↔ (𝐶 ∈ V ∧ 𝐵 ∈ V)))
3		preq2 4684	. . . 4 ⊢ (𝐴 = 𝐵 → {𝐶, 𝐴} = {𝐶, 𝐵})
4	3	preq2d 4690	. . 3 ⊢ (𝐴 = 𝐵 → {{𝐶}, {𝐶, 𝐴}} = {{𝐶}, {𝐶, 𝐵}})
5	2, 4	ifbieq1d 4497	. 2 ⊢ (𝐴 = 𝐵 → if((𝐶 ∈ V ∧ 𝐴 ∈ V), {{𝐶}, {𝐶, 𝐴}}, ∅) = if((𝐶 ∈ V ∧ 𝐵 ∈ V), {{𝐶}, {𝐶, 𝐵}}, ∅))
6		dfopif 4819	. 2 ⊢ ⟨𝐶, 𝐴⟩ = if((𝐶 ∈ V ∧ 𝐴 ∈ V), {{𝐶}, {𝐶, 𝐴}}, ∅)
7		dfopif 4819	. 2 ⊢ ⟨𝐶, 𝐵⟩ = if((𝐶 ∈ V ∧ 𝐵 ∈ V), {{𝐶}, {𝐶, 𝐵}}, ∅)
8	5, 6, 7	3eqtr4g 2791	1 ⊢ (𝐴 = 𝐵 → ⟨𝐶, 𝐴⟩ = ⟨𝐶, 𝐵⟩)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1541   ∈ wcel 2111  Vcvv 3436  ∅c0 4280  ifcif 4472  {csn 4573  {cpr 4575  ⟨cop 4579

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-rab 3396  df-v 3438  df-dif 3900  df-un 3902  df-ss 3914  df-nul 4281  df-if 4473  df-sn 4574  df-pr 4576  df-op 4580

This theorem is referenced by:  opeq12  4824  opeq2i  4826  opeq2d  4829  oteq2  4832  oteq3  4833  breq2  5093  cbvopab2  5165  cbvopab2v  5168  opthg  5415  eqvinop  5425  opelopabsb  5468  dfid3  5512  opelxp  5650  relopabi  5761  opabid2  5767  elrn2g  5829  opeldmd  5845  opeldm  5846  iss  5983  elidinxp  5992  dmsnopg  6160  reuop  6240  funopg  6515  f1osng  6804  f1oprswap  6807  tz6.12f  6847  fvn0ssdmfun  7007  fsn  7068  fsng  7070  fprg  7088  fprb  7128  oveq2  7354  cbvoprab2  7434  cbvoprab3v  7438  ovg  7511  elxp4  7852  elxp5  7853  opabex3d  7897  opabex3rd  7898  opabex3  7899  op1stg  7933  op2ndg  7934  op1steq  7965  dfoprab4f  7988  fsplit  8047  xpord2pred  8075  seqomlem2  8370  omeu  8500  oeeui  8517  ralxpmap  8820  elixpsn  8861  ixpsnf1o  8862  mapsnend  8958  xpsnen  8974  xpassen  8984  xpf1o  9052  unxpdomlem1  9140  djulcl  9803  djurcl  9804  djur  9812  djuss  9813  djuun  9819  1stinl  9820  2ndinl  9821  1stinr  9822  2ndinr  9823  axdc4lem  10346  nqereu  10820  mulcanenq  10851  elreal  11022  ax1rid  11052  fseq1p1m1  13498  pfxval  14581  swrdccatin1  14632  swrdccat3blem  14646  wrdlen2  14851  ruclem1  16140  imasaddfnlem  17432  imasvscafn  17441  catidex  17580  catpropd  17615  funcsetcestrclem1  18060  symg2bas  19305  efgi  19631  gsumcom2  19887  pzriprnglem3  21420  pzriprnglem10  21427  mat1rhmval  22394  mat1ric  22402  txkgen  23567  cnmpt21  23586  xkoinjcn  23602  txconn  23604  xpstopnlem1  23724  qustgplem  24036  metustid  24469  axlowdim2  28938  axlowdim  28939  axcontlem2  28943  axcontlem3  28944  axcontlem4  28945  axcontlem9  28950  axcontlem10  28951  axcontlem11  28952  cusgrexg  29422  rgrusgrprc  29568  2clwwlk2clwwlk  30330  isnvlem  30590  br8d  32591  gsumhashmul  33041  prsdm  33927  eulerpartlemgvv  34389  reprsuc  34628  bnj941  34784  bnj944  34950  fineqvrep  35137  cvmlift2lem1  35346  cvmlift2lem12  35358  goel  35391  gonafv  35394  satf0op  35421  sat1el2xp  35423  fmla0xp  35427  sategoelfvb  35463  br8  35800  br6  35801  br4  35802  dfrn5  35818  elima4  35820  pprodss4v  35926  brimg  35979  brapply  35980  brsuccf  35983  brrestrict  35991  dfrdg4  35993  cgrtriv  36044  brofs  36047  segconeu  36053  btwntriv2  36054  transportprops  36076  brifs  36085  ifscgr  36086  brcgr3  36088  cgrxfr  36097  brcolinear2  36100  colineardim1  36103  brfs  36121  idinside  36126  btwnconn1lem7  36135  btwnconn1lem11  36139  btwnconn1lem12  36140  btwnconn1lem14  36142  brsegle  36150  seglerflx  36154  seglemin  36155  segleantisym  36157  btwnsegle  36159  outsideofeu  36173  outsidele  36174  linedegen  36185  fvline  36186  cbvoprab2vw  36280  cbvoprab23vw  36282  cbvopab2davw  36307  cbvoprab2davw  36314  finxpreclem6  37438  finxpsuclem  37439  curfv  37648  poimirlem4  37672  poimirlem26  37694  isdivrngo  37998  drngoi  37999  iss2  38380  dibelval3  41194  diblsmopel  41218  dihjatcclem4  41468  frlmsnic  42581  dfhe3  43816  dffrege115  44019  dropab2  44488  relopabVD  44941  projf1o  45242  sge0xp  46475  hoidmv1le  46640  fsetsniunop  47088  fsetsnf  47090  fsetsnf1  47091  fsetsnfo  47092  ichnreuop  47511  ichreuopeq  47512  reuopreuprim  47565  gpgprismgriedgdmss  48091  gpgvtx0  48092  gpgvtx1  48093  gpgedgvtx0  48100  gpgedgvtx1  48101  gpgedgiov  48104  gpgedg2ov  48105  gpgedg2iv  48106  gpg3kgrtriexlem6  48127  gpgprismgr4cycllem3  48136  pgnbgreunbgrlem1  48152  pgnbgreunbgrlem2  48156  pgnbgreunbgrlem4  48158  pgnbgreunbgrlem5lem1  48159  pgnbgreunbgrlem5lem2  48160  pgnbgreunbgrlem5lem3  48161  pgnbgreunbgrlem5  48162  gpg5edgnedg  48169  0aryfvalel  48674  1arymaptf1  48682  2arymaptf1  48693  prelrrx2b  48754  rrx2xpref1o  48758  rrx2plordisom  48763  sectpropdlem  49076  ssccatid  49112  isthincd2lem2  49475