Theorem opeq2 4825

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 4686	. . . 4 ⊢ (𝐴 = 𝐵 → {𝐶, 𝐴} = {𝐶, 𝐵})
4	3	preq2d 4692	. . 3 ⊢ (𝐴 = 𝐵 → {{𝐶}, {𝐶, 𝐴}} = {{𝐶}, {𝐶, 𝐵}})
5	2, 4	ifbieq1d 4501	. 2 ⊢ (𝐴 = 𝐵 → if((𝐶 ∈ V ∧ 𝐴 ∈ V), {{𝐶}, {𝐶, 𝐴}}, ∅) = if((𝐶 ∈ V ∧ 𝐵 ∈ V), {{𝐶}, {𝐶, 𝐵}}, ∅))
6		dfopif 4821	. 2 ⊢ ⟨𝐶, 𝐴⟩ = if((𝐶 ∈ V ∧ 𝐴 ∈ V), {{𝐶}, {𝐶, 𝐴}}, ∅)
7		dfopif 4821	. 2 ⊢ ⟨𝐶, 𝐵⟩ = if((𝐶 ∈ V ∧ 𝐵 ∈ V), {{𝐶}, {𝐶, 𝐵}}, ∅)
8	5, 6, 7	3eqtr4g 2789	1 ⊢ (𝐴 = 𝐵 → ⟨𝐶, 𝐴⟩ = ⟨𝐶, 𝐵⟩)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2109  Vcvv 3436  ∅c0 4284  ifcif 4476  {csn 4577  {cpr 4579  ⟨cop 4583

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 3395  df-v 3438  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584

This theorem is referenced by:  opeq12  4826  opeq2i  4828  opeq2d  4831  oteq2  4834  oteq3  4835  breq2  5096  cbvopab2  5168  cbvopab2v  5171  opthg  5420  eqvinop  5430  opelopabsb  5473  dfid3  5517  opelxp  5655  relopabi  5765  opabid2  5771  elrn2g  5833  opeldmd  5849  opeldm  5850  iss  5986  elidinxp  5995  dmsnopg  6162  reuop  6241  funopg  6516  f1osng  6805  f1oprswap  6808  tz6.12f  6847  fvn0ssdmfun  7008  fsn  7069  fsng  7071  fprg  7089  fprb  7130  oveq2  7357  cbvoprab2  7437  cbvoprab3v  7441  ovg  7514  elxp4  7855  elxp5  7856  opabex3d  7900  opabex3rd  7901  opabex3  7902  op1stg  7936  op2ndg  7937  op1steq  7968  dfoprab4f  7991  fsplit  8050  xpord2pred  8078  seqomlem2  8373  omeu  8503  oeeui  8520  ralxpmap  8823  elixpsn  8864  ixpsnf1o  8865  mapsnend  8961  xpsnen  8978  xpassen  8988  xpf1o  9056  unxpdomlem1  9145  djulcl  9806  djurcl  9807  djur  9815  djuss  9816  djuun  9822  1stinl  9823  2ndinl  9824  1stinr  9825  2ndinr  9826  axdc4lem  10349  nqereu  10823  mulcanenq  10854  elreal  11025  ax1rid  11055  fseq1p1m1  13501  pfxval  14580  swrdccatin1  14631  swrdccat3blem  14645  wrdlen2  14851  ruclem1  16140  imasaddfnlem  17432  imasvscafn  17441  catidex  17580  catpropd  17615  funcsetcestrclem1  18060  symg2bas  19272  efgi  19598  gsumcom2  19854  pzriprnglem3  21390  pzriprnglem10  21397  mat1rhmval  22364  mat1ric  22372  txkgen  23537  cnmpt21  23556  xkoinjcn  23572  txconn  23574  xpstopnlem1  23694  qustgplem  24006  metustid  24440  axlowdim2  28905  axlowdim  28906  axcontlem2  28910  axcontlem3  28911  axcontlem4  28912  axcontlem9  28917  axcontlem10  28918  axcontlem11  28919  cusgrexg  29389  rgrusgrprc  29535  2clwwlk2clwwlk  30294  isnvlem  30554  br8d  32555  gsumhashmul  33014  prsdm  33881  eulerpartlemgvv  34344  reprsuc  34583  bnj941  34739  bnj944  34905  fineqvrep  35070  cvmlift2lem1  35275  cvmlift2lem12  35287  goel  35320  gonafv  35323  satf0op  35350  sat1el2xp  35352  fmla0xp  35356  sategoelfvb  35392  br8  35729  br6  35730  br4  35731  dfrn5  35747  elima4  35749  pprodss4v  35858  brimg  35911  brapply  35912  brsuccf  35915  brrestrict  35923  dfrdg4  35925  cgrtriv  35976  brofs  35979  segconeu  35985  btwntriv2  35986  transportprops  36008  brifs  36017  ifscgr  36018  brcgr3  36020  cgrxfr  36029  brcolinear2  36032  colineardim1  36035  brfs  36053  idinside  36058  btwnconn1lem7  36067  btwnconn1lem11  36071  btwnconn1lem12  36072  btwnconn1lem14  36074  brsegle  36082  seglerflx  36086  seglemin  36087  segleantisym  36089  btwnsegle  36091  outsideofeu  36105  outsidele  36106  linedegen  36117  fvline  36118  cbvoprab2vw  36212  cbvoprab23vw  36214  cbvopab2davw  36239  cbvoprab2davw  36246  finxpreclem6  37370  finxpsuclem  37371  curfv  37580  poimirlem4  37604  poimirlem26  37626  isdivrngo  37930  drngoi  37931  iss2  38312  dibelval3  41126  diblsmopel  41150  dihjatcclem4  41400  frlmsnic  42513  dfhe3  43748  dffrege115  43951  dropab2  44421  relopabVD  44874  projf1o  45175  sge0xp  46410  hoidmv1le  46575  fsetsniunop  47033  fsetsnf  47035  fsetsnf1  47036  fsetsnfo  47037  ichnreuop  47456  ichreuopeq  47457  reuopreuprim  47510  gpgprismgriedgdmss  48036  gpgvtx0  48037  gpgvtx1  48038  gpgedgvtx0  48045  gpgedgvtx1  48046  gpgedgiov  48049  gpgedg2ov  48050  gpgedg2iv  48051  gpg3kgrtriexlem6  48072  gpgprismgr4cycllem3  48081  pgnbgreunbgrlem1  48097  pgnbgreunbgrlem2  48101  pgnbgreunbgrlem4  48103  pgnbgreunbgrlem5lem1  48104  pgnbgreunbgrlem5lem2  48105  pgnbgreunbgrlem5lem3  48106  pgnbgreunbgrlem5  48107  gpg5edgnedg  48114  0aryfvalel  48619  1arymaptf1  48627  2arymaptf1  48638  prelrrx2b  48699  rrx2xpref1o  48703  rrx2plordisom  48708  sectpropdlem  49021  ssccatid  49057  isthincd2lem2  49420