Theorem opeq2 4805

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 2827	. . . 4 ⊢ (𝐴 = 𝐵 → (𝐴 ∈ V ↔ 𝐵 ∈ V))
2	1	anbi2d 636	. . 3 ⊢ (𝐴 = 𝐵 → ((𝐶 ∈ V ∧ 𝐴 ∈ V) ↔ (𝐶 ∈ V ∧ 𝐵 ∈ V)))
3		preq2 4666	. . . 4 ⊢ (𝐴 = 𝐵 → {𝐶, 𝐴} = {𝐶, 𝐵})
4	3	preq2d 4672	. . 3 ⊢ (𝐴 = 𝐵 → {{𝐶}, {𝐶, 𝐴}} = {{𝐶}, {𝐶, 𝐵}})
5	2, 4	ifbieq1d 4479	. 2 ⊢ (𝐴 = 𝐵 → if((𝐶 ∈ V ∧ 𝐴 ∈ V), {{𝐶}, {𝐶, 𝐴}}, ∅) = if((𝐶 ∈ V ∧ 𝐵 ∈ V), {{𝐶}, {𝐶, 𝐵}}, ∅))
6		dfopif 4801	. 2 ⊢ ⟨𝐶, 𝐴⟩ = if((𝐶 ∈ V ∧ 𝐴 ∈ V), {{𝐶}, {𝐶, 𝐴}}, ∅)
7		dfopif 4801	. 2 ⊢ ⟨𝐶, 𝐵⟩ = if((𝐶 ∈ V ∧ 𝐵 ∈ V), {{𝐶}, {𝐶, 𝐵}}, ∅)
8	5, 6, 7	3eqtr4g 2799	1 ⊢ (𝐴 = 𝐵 → ⟨𝐶, 𝐴⟩ = ⟨𝐶, 𝐵⟩)

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1547   ∈ wcel 2119  Vcvv 3431  ∅c0 4261  ifcif 4454  {csn 4555  {cpr 4557  ⟨cop 4561

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-rab 3392  df-v 3433  df-dif 3886  df-un 3888  df-ss 3900  df-nul 4262  df-if 4455  df-sn 4556  df-pr 4558  df-op 4562

This theorem is referenced by:  opeq12  4806  opeq2i  4808  opeq2d  4811  oteq2  4814  oteq3  4815  breq2  5076  cbvopab2  5148  cbvopab2v  5151  opthg  5417  eqvinop  5427  opelopabsb  5472  dfid3  5516  opelxp  5654  relopabi  5765  opabid2  5771  elrn2g  5832  opeldmd  5848  opeldm  5849  iss  5987  elidinxp  5996  dmsnopg  6164  reuop  6244  funopg  6519  f1osng  6809  f1oprswap  6812  tz6.12f  6852  fvn0ssdmfun  7015  fsn  7077  fsng  7079  fprg  7098  fprb  7138  oveq2  7364  cbvoprab2  7444  cbvoprab3v  7448  ovg  7521  elxp4  7862  elxp5  7863  opabex3d  7907  opabex3rd  7908  opabex3  7909  op1stg  7943  op2ndg  7944  op1steq  7975  dfoprab4f  7998  fsplit  8056  xpord2pred  8085  seqomlem2  8380  omeu  8510  oeeui  8528  ralxpmap  8834  elixpsn  8875  ixpsnf1o  8876  mapsnend  8973  xpsnen  8989  xpassen  8999  xpf1o  9067  unxpdomlem1  9156  djulcl  9825  djurcl  9826  djur  9834  djuss  9835  djuun  9841  1stinl  9842  2ndinl  9843  1stinr  9844  2ndinr  9845  axdc4lem  10368  nqereu  10843  mulcanenq  10874  elreal  11045  ax1rid  11075  fseq1p1m1  13543  pfxval  14627  swrdccatin1  14678  swrdccat3blem  14692  wrdlen2  14897  ruclem1  16189  imasaddfnlem  17483  imasvscafn  17492  catidex  17631  catpropd  17666  funcsetcestrclem1  18111  symg2bas  19359  efgi  19685  gsumcom2  19941  pzriprnglem3  21458  pzriprnglem10  21465  mat1rhmval  22462  mat1ric  22470  txkgen  23635  cnmpt21  23654  xkoinjcn  23670  txconn  23672  xpstopnlem1  23792  qustgplem  24104  metustid  24537  axlowdim2  29047  axlowdim  29048  axcontlem2  29052  axcontlem3  29053  axcontlem4  29054  axcontlem9  29059  axcontlem10  29060  axcontlem11  29061  cusgrexg  29531  rgrusgrprc  29676  2clwwlk2clwwlk  30438  isnvlem  30699  br8d  32700  gsumhashmul  33148  prsdm  34098  eulerpartlemgvv  34560  reprsuc  34799  bnj941  34955  bnj944  35120  fineqvrep  35295  cvmlift2lem1  35530  cvmlift2lem12  35542  goel  35575  gonafv  35578  satf0op  35605  sat1el2xp  35607  fmla0xp  35611  sategoelfvb  35647  br8  35984  br6  35985  br4  35986  dfrn5  36002  elima4  36004  pprodss4v  36110  brimg  36163  brapply  36164  lemsuccf  36167  brrestrict  36177  dfrdg4  36179  cgrtriv  36230  brofs  36233  segconeu  36239  btwntriv2  36240  transportprops  36262  brifs  36271  ifscgr  36272  brcgr3  36274  cgrxfr  36283  brcolinear2  36286  colineardim1  36289  brfs  36307  idinside  36312  btwnconn1lem7  36321  btwnconn1lem11  36325  btwnconn1lem12  36326  btwnconn1lem14  36328  brsegle  36336  seglerflx  36340  seglemin  36341  segleantisym  36343  btwnsegle  36345  outsideofeu  36359  outsidele  36360  linedegen  36371  fvline  36372  cbvoprab2vw  36466  cbvoprab23vw  36468  cbvopab2davw  36493  cbvoprab2davw  36500  finxpreclem6  37758  finxpsuclem  37759  curfv  37967  poimirlem4  37991  poimirlem26  38013  isdivrngo  38317  drngoi  38318  iss2  38711  dibelval3  41639  diblsmopel  41663  dihjatcclem4  41913  frlmsnic  43026  dfhe3  44219  dffrege115  44422  dropab2  44891  relopabVD  45344  projf1o  45643  sge0xp  46872  hoidmv1le  47037  fsetsniunop  47512  fsetsnf  47514  fsetsnf1  47515  fsetsnfo  47516  ichnreuop  47947  ichreuopeq  47948  reuopreuprim  48001  gpgprismgriedgdmss  48543  gpgvtx0  48544  gpgvtx1  48545  gpgedgvtx0  48552  gpgedgvtx1  48553  gpgedgiov  48556  gpgedg2ov  48557  gpgedg2iv  48558  gpg3kgrtriexlem6  48579  gpgprismgr4cycllem3  48588  pgnbgreunbgrlem1  48604  pgnbgreunbgrlem2  48608  pgnbgreunbgrlem4  48610  pgnbgreunbgrlem5lem1  48611  pgnbgreunbgrlem5lem2  48612  pgnbgreunbgrlem5lem3  48613  pgnbgreunbgrlem5  48614  gpg5edgnedg  48621  0aryfvalel  49125  1arymaptf1  49133  2arymaptf1  49144  prelrrx2b  49205  rrx2xpref1o  49209  rrx2plordisom  49214  sectpropdlem  49526  ssccatid  49562  isthincd2lem2  49925