Theorem opeq2 4796

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 2898	. . . 4 ⊢ (𝐴 = 𝐵 → (𝐴 ∈ V ↔ 𝐵 ∈ V))
2	1	anbi2d 630	. . 3 ⊢ (𝐴 = 𝐵 → ((𝐶 ∈ V ∧ 𝐴 ∈ V) ↔ (𝐶 ∈ V ∧ 𝐵 ∈ V)))
3		preq2 4662	. . . 4 ⊢ (𝐴 = 𝐵 → {𝐶, 𝐴} = {𝐶, 𝐵})
4	3	preq2d 4668	. . 3 ⊢ (𝐴 = 𝐵 → {{𝐶}, {𝐶, 𝐴}} = {{𝐶}, {𝐶, 𝐵}})
5	2, 4	ifbieq1d 4488	. 2 ⊢ (𝐴 = 𝐵 → if((𝐶 ∈ V ∧ 𝐴 ∈ V), {{𝐶}, {𝐶, 𝐴}}, ∅) = if((𝐶 ∈ V ∧ 𝐵 ∈ V), {{𝐶}, {𝐶, 𝐵}}, ∅))
6		dfopif 4792	. 2 ⊢ ⟨𝐶, 𝐴⟩ = if((𝐶 ∈ V ∧ 𝐴 ∈ V), {{𝐶}, {𝐶, 𝐴}}, ∅)
7		dfopif 4792	. 2 ⊢ ⟨𝐶, 𝐵⟩ = if((𝐶 ∈ V ∧ 𝐵 ∈ V), {{𝐶}, {𝐶, 𝐵}}, ∅)
8	5, 6, 7	3eqtr4g 2879	1 ⊢ (𝐴 = 𝐵 → ⟨𝐶, 𝐴⟩ = ⟨𝐶, 𝐵⟩)

Syntax hints:   → wi 4   ∧ wa 398   = wceq 1531   ∈ wcel 2108  Vcvv 3493  ∅c0 4289  ifcif 4465  {csn 4559  {cpr 4561  ⟨cop 4565

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1905  ax-6 1964  ax-7 2009  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2154  ax-12 2170  ax-ext 2791

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1084  df-tru 1534  df-ex 1775  df-nf 1779  df-sb 2064  df-clab 2798  df-cleq 2812  df-clel 2891  df-nfc 2961  df-rab 3145  df-v 3495  df-dif 3937  df-un 3939  df-in 3941  df-ss 3950  df-nul 4290  df-if 4466  df-sn 4560  df-pr 4562  df-op 4566

This theorem is referenced by:  opeq12  4797  opeq2i  4799  opeq2d  4802  oteq2  4805  oteq3  4806  breq2  5061  cbvopab2  5132  cbvopab2v  5135  opthg  5360  eqvinop  5369  opelopabsb  5408  dfid3  5455  opelxp  5584  relopabi  5687  opabid2  5693  elrn2g  5754  opeldmd  5768  opeldm  5769  elrn2  5814  iss  5896  elidinxp  5904  elimasng  5948  dmsnopg  6063  reuop  6137  funopg  6382  f1osng  6648  f1oprswap  6651  tz6.12f  6687  fvn0ssdmfun  6835  fsn  6890  fsng  6892  fprg  6910  fprb  6949  oveq2  7156  cbvoprab2  7234  ovg  7305  elxp4  7619  elxp5  7620  opabex3d  7658  opabex3rd  7659  opabex3  7660  op1stg  7693  op2ndg  7694  op1steq  7725  dfoprab4f  7746  fsplit  7804  seqomlem2  8079  omeu  8203  oeeui  8220  ralxpmap  8452  elixpsn  8493  ixpsnf1o  8494  mapsnend  8580  xpsnen  8593  xpassen  8603  xpf1o  8671  unxpdomlem1  8714  djulcl  9331  djurcl  9332  djur  9340  djuss  9341  djuun  9347  1stinl  9348  2ndinl  9349  1stinr  9350  2ndinr  9351  axdc4lem  9869  nqereu  10343  mulcanenq  10374  elreal  10545  ax1rid  10575  fseq1p1m1  12973  pfxval  14027  swrdccatin1  14079  swrdccat3blem  14093  wrdlen2  14298  ruclem1  15576  imasaddfnlem  16793  imasvscafn  16802  catidex  16937  catpropd  16971  funcsetcestrclem1  17396  symg2bas  18513  efgi  18837  gsumcom2  19087  mat1rhmval  21080  mat1ric  21088  txkgen  22252  cnmpt21  22271  xkoinjcn  22287  txconn  22289  xpstopnlem1  22409  qustgplem  22721  metustid  23156  axlowdim2  26738  axlowdim  26739  axcontlem2  26743  axcontlem3  26744  axcontlem4  26745  axcontlem9  26750  axcontlem10  26751  axcontlem11  26752  cusgrexg  27218  rgrusgrprc  27363  2clwwlk2clwwlk  28121  isnvlem  28379  br8d  30353  prsdm  31150  eulerpartlemgvv  31627  reprsuc  31879  bnj941  32037  bnj944  32203  cvmlift2lem1  32542  cvmlift2lem12  32554  goel  32587  gonafv  32590  satf0op  32617  sat1el2xp  32619  fmla0xp  32623  sategoelfvb  32659  br8  32985  br6  32986  br4  32987  dfrn5  33010  elima4  33012  pprodss4v  33338  brimg  33391  brapply  33392  brsuccf  33395  brrestrict  33403  dfrdg4  33405  cgrtriv  33456  brofs  33459  segconeu  33465  btwntriv2  33466  transportprops  33488  brifs  33497  ifscgr  33498  brcgr3  33500  cgrxfr  33509  brcolinear2  33512  colineardim1  33515  brfs  33533  idinside  33538  btwnconn1lem7  33547  btwnconn1lem11  33551  btwnconn1lem12  33552  btwnconn1lem14  33554  brsegle  33562  seglerflx  33566  seglemin  33567  segleantisym  33569  btwnsegle  33571  outsideofeu  33585  outsidele  33586  linedegen  33597  fvline  33598  finxpreclem6  34669  finxpsuclem  34670  curfv  34864  poimirlem4  34888  poimirlem26  34910  isdivrngo  35220  drngoi  35221  iss2  35593  dibelval3  38275  diblsmopel  38299  dihjatcclem4  38549  frlmsnic  39139  dfhe3  40111  dffrege115  40314  dropab2  40770  relopabVD  41225  projf1o  41448  sge0xp  42701  hoidmv1le  42866  ichnreuop  43624  ichreuopeq  43625  reuopreuprim  43678  prelrrx2b  44691  rrx2xpref1o  44695  rrx2plordisom  44700