Theorem opeq2 4838

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 2816	. . . 4 ⊢ (𝐴 = 𝐵 → (𝐴 ∈ V ↔ 𝐵 ∈ V))
2	1	anbi2d 630	. . 3 ⊢ (𝐴 = 𝐵 → ((𝐶 ∈ V ∧ 𝐴 ∈ V) ↔ (𝐶 ∈ V ∧ 𝐵 ∈ V)))
3		preq2 4698	. . . 4 ⊢ (𝐴 = 𝐵 → {𝐶, 𝐴} = {𝐶, 𝐵})
4	3	preq2d 4704	. . 3 ⊢ (𝐴 = 𝐵 → {{𝐶}, {𝐶, 𝐴}} = {{𝐶}, {𝐶, 𝐵}})
5	2, 4	ifbieq1d 4513	. 2 ⊢ (𝐴 = 𝐵 → if((𝐶 ∈ V ∧ 𝐴 ∈ V), {{𝐶}, {𝐶, 𝐴}}, ∅) = if((𝐶 ∈ V ∧ 𝐵 ∈ V), {{𝐶}, {𝐶, 𝐵}}, ∅))
6		dfopif 4834	. 2 ⊢ ⟨𝐶, 𝐴⟩ = if((𝐶 ∈ V ∧ 𝐴 ∈ V), {{𝐶}, {𝐶, 𝐴}}, ∅)
7		dfopif 4834	. 2 ⊢ ⟨𝐶, 𝐵⟩ = if((𝐶 ∈ V ∧ 𝐵 ∈ V), {{𝐶}, {𝐶, 𝐵}}, ∅)
8	5, 6, 7	3eqtr4g 2789	1 ⊢ (𝐴 = 𝐵 → ⟨𝐶, 𝐴⟩ = ⟨𝐶, 𝐵⟩)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2109  Vcvv 3447  ∅c0 4296  ifcif 4488  {csn 4589  {cpr 4591  ⟨cop 4595

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 2701

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 2708  df-cleq 2721  df-clel 2803  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596

This theorem is referenced by:  opeq12  4839  opeq2i  4841  opeq2d  4844  oteq2  4847  oteq3  4848  breq2  5111  cbvopab2  5183  cbvopab2v  5186  opthg  5437  eqvinop  5447  opelopabsb  5490  dfid3  5536  opelxp  5674  relopabi  5785  opabid2  5791  elrn2g  5854  opeldmd  5870  opeldm  5871  iss  6006  elidinxp  6015  dmsnopg  6186  reuop  6266  funopg  6550  f1osng  6841  f1oprswap  6844  tz6.12f  6884  fvn0ssdmfun  7046  fsn  7107  fsng  7109  fprg  7127  fprb  7168  oveq2  7395  cbvoprab2  7477  cbvoprab3v  7481  ovg  7554  elxp4  7898  elxp5  7899  opabex3d  7944  opabex3rd  7945  opabex3  7946  op1stg  7980  op2ndg  7981  op1steq  8012  dfoprab4f  8035  fsplit  8096  xpord2pred  8124  seqomlem2  8419  omeu  8549  oeeui  8566  ralxpmap  8869  elixpsn  8910  ixpsnf1o  8911  mapsnend  9007  xpsnen  9025  xpassen  9035  xpf1o  9103  unxpdomlem1  9197  djulcl  9863  djurcl  9864  djur  9872  djuss  9873  djuun  9879  1stinl  9880  2ndinl  9881  1stinr  9882  2ndinr  9883  axdc4lem  10408  nqereu  10882  mulcanenq  10913  elreal  11084  ax1rid  11114  fseq1p1m1  13559  pfxval  14638  swrdccatin1  14690  swrdccat3blem  14704  wrdlen2  14910  ruclem1  16199  imasaddfnlem  17491  imasvscafn  17500  catidex  17635  catpropd  17670  funcsetcestrclem1  18115  symg2bas  19323  efgi  19649  gsumcom2  19905  pzriprnglem3  21393  pzriprnglem10  21400  mat1rhmval  22366  mat1ric  22374  txkgen  23539  cnmpt21  23558  xkoinjcn  23574  txconn  23576  xpstopnlem1  23696  qustgplem  24008  metustid  24442  axlowdim2  28887  axlowdim  28888  axcontlem2  28892  axcontlem3  28893  axcontlem4  28894  axcontlem9  28899  axcontlem10  28900  axcontlem11  28901  cusgrexg  29371  rgrusgrprc  29517  2clwwlk2clwwlk  30279  isnvlem  30539  br8d  32538  gsumhashmul  33001  prsdm  33904  eulerpartlemgvv  34367  reprsuc  34606  bnj941  34762  bnj944  34928  fineqvrep  35085  cvmlift2lem1  35289  cvmlift2lem12  35301  goel  35334  gonafv  35337  satf0op  35364  sat1el2xp  35366  fmla0xp  35370  sategoelfvb  35406  br8  35743  br6  35744  br4  35745  dfrn5  35761  elima4  35763  pprodss4v  35872  brimg  35925  brapply  35926  brsuccf  35929  brrestrict  35937  dfrdg4  35939  cgrtriv  35990  brofs  35993  segconeu  35999  btwntriv2  36000  transportprops  36022  brifs  36031  ifscgr  36032  brcgr3  36034  cgrxfr  36043  brcolinear2  36046  colineardim1  36049  brfs  36067  idinside  36072  btwnconn1lem7  36081  btwnconn1lem11  36085  btwnconn1lem12  36086  btwnconn1lem14  36088  brsegle  36096  seglerflx  36100  seglemin  36101  segleantisym  36103  btwnsegle  36105  outsideofeu  36119  outsidele  36120  linedegen  36131  fvline  36132  cbvoprab2vw  36226  cbvoprab23vw  36228  cbvopab2davw  36253  cbvoprab2davw  36260  finxpreclem6  37384  finxpsuclem  37385  curfv  37594  poimirlem4  37618  poimirlem26  37640  isdivrngo  37944  drngoi  37945  iss2  38326  dibelval3  41141  diblsmopel  41165  dihjatcclem4  41415  frlmsnic  42528  dfhe3  43764  dffrege115  43967  dropab2  44437  relopabVD  44890  projf1o  45191  sge0xp  46427  hoidmv1le  46592  fsetsniunop  47050  fsetsnf  47052  fsetsnf1  47053  fsetsnfo  47054  ichnreuop  47473  ichreuopeq  47474  reuopreuprim  47527  gpgprismgriedgdmss  48043  gpgvtx0  48044  gpgvtx1  48045  gpgedgvtx0  48052  gpgedgvtx1  48053  gpgedgiov  48056  gpgedg2ov  48057  gpgedg2iv  48058  gpg3kgrtriexlem6  48079  gpgprismgr4cycllem3  48087  pgnbgreunbgrlem1  48103  pgnbgreunbgrlem2  48107  pgnbgreunbgrlem4  48109  pgnbgreunbgrlem5lem1  48110  pgnbgreunbgrlem5lem2  48111  pgnbgreunbgrlem5lem3  48112  pgnbgreunbgrlem5  48113  0aryfvalel  48623  1arymaptf1  48631  2arymaptf1  48642  prelrrx2b  48703  rrx2xpref1o  48707  rrx2plordisom  48712  sectpropdlem  49025  ssccatid  49061  isthincd2lem2  49424