Theorem opeq2 4834

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2109  Vcvv 3444  ∅c0 4292  ifcif 4484  {csn 4585  {cpr 4587  ⟨cop 4591

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 3403  df-v 3446  df-dif 3914  df-un 3916  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592

This theorem is referenced by:  opeq12  4835  opeq2i  4837  opeq2d  4840  oteq2  4843  oteq3  4844  breq2  5106  cbvopab2  5178  cbvopab2v  5181  opthg  5432  eqvinop  5442  opelopabsb  5485  dfid3  5529  opelxp  5667  relopabi  5776  opabid2  5782  elrn2g  5844  opeldmd  5860  opeldm  5861  iss  5995  elidinxp  6004  dmsnopg  6174  reuop  6254  funopg  6534  f1osng  6823  f1oprswap  6826  tz6.12f  6866  fvn0ssdmfun  7028  fsn  7089  fsng  7091  fprg  7109  fprb  7150  oveq2  7377  cbvoprab2  7457  cbvoprab3v  7461  ovg  7534  elxp4  7878  elxp5  7879  opabex3d  7923  opabex3rd  7924  opabex3  7925  op1stg  7959  op2ndg  7960  op1steq  7991  dfoprab4f  8014  fsplit  8073  xpord2pred  8101  seqomlem2  8396  omeu  8526  oeeui  8543  ralxpmap  8846  elixpsn  8887  ixpsnf1o  8888  mapsnend  8984  xpsnen  9002  xpassen  9012  xpf1o  9080  unxpdomlem1  9173  djulcl  9839  djurcl  9840  djur  9848  djuss  9849  djuun  9855  1stinl  9856  2ndinl  9857  1stinr  9858  2ndinr  9859  axdc4lem  10384  nqereu  10858  mulcanenq  10889  elreal  11060  ax1rid  11090  fseq1p1m1  13535  pfxval  14614  swrdccatin1  14666  swrdccat3blem  14680  wrdlen2  14886  ruclem1  16175  imasaddfnlem  17467  imasvscafn  17476  catidex  17611  catpropd  17646  funcsetcestrclem1  18091  symg2bas  19299  efgi  19625  gsumcom2  19881  pzriprnglem3  21369  pzriprnglem10  21376  mat1rhmval  22342  mat1ric  22350  txkgen  23515  cnmpt21  23534  xkoinjcn  23550  txconn  23552  xpstopnlem1  23672  qustgplem  23984  metustid  24418  axlowdim2  28863  axlowdim  28864  axcontlem2  28868  axcontlem3  28869  axcontlem4  28870  axcontlem9  28875  axcontlem10  28876  axcontlem11  28877  cusgrexg  29347  rgrusgrprc  29493  2clwwlk2clwwlk  30252  isnvlem  30512  br8d  32511  gsumhashmul  32974  prsdm  33877  eulerpartlemgvv  34340  reprsuc  34579  bnj941  34735  bnj944  34901  fineqvrep  35058  cvmlift2lem1  35262  cvmlift2lem12  35274  goel  35307  gonafv  35310  satf0op  35337  sat1el2xp  35339  fmla0xp  35343  sategoelfvb  35379  br8  35716  br6  35717  br4  35718  dfrn5  35734  elima4  35736  pprodss4v  35845  brimg  35898  brapply  35899  brsuccf  35902  brrestrict  35910  dfrdg4  35912  cgrtriv  35963  brofs  35966  segconeu  35972  btwntriv2  35973  transportprops  35995  brifs  36004  ifscgr  36005  brcgr3  36007  cgrxfr  36016  brcolinear2  36019  colineardim1  36022  brfs  36040  idinside  36045  btwnconn1lem7  36054  btwnconn1lem11  36058  btwnconn1lem12  36059  btwnconn1lem14  36061  brsegle  36069  seglerflx  36073  seglemin  36074  segleantisym  36076  btwnsegle  36078  outsideofeu  36092  outsidele  36093  linedegen  36104  fvline  36105  cbvoprab2vw  36199  cbvoprab23vw  36201  cbvopab2davw  36226  cbvoprab2davw  36233  finxpreclem6  37357  finxpsuclem  37358  curfv  37567  poimirlem4  37591  poimirlem26  37613  isdivrngo  37917  drngoi  37918  iss2  38299  dibelval3  41114  diblsmopel  41138  dihjatcclem4  41388  frlmsnic  42501  dfhe3  43737  dffrege115  43940  dropab2  44410  relopabVD  44863  projf1o  45164  sge0xp  46400  hoidmv1le  46565  fsetsniunop  47023  fsetsnf  47025  fsetsnf1  47026  fsetsnfo  47027  ichnreuop  47446  ichreuopeq  47447  reuopreuprim  47500  gpgprismgriedgdmss  48016  gpgvtx0  48017  gpgvtx1  48018  gpgedgvtx0  48025  gpgedgvtx1  48026  gpgedgiov  48029  gpgedg2ov  48030  gpgedg2iv  48031  gpg3kgrtriexlem6  48052  gpgprismgr4cycllem3  48060  pgnbgreunbgrlem1  48076  pgnbgreunbgrlem2  48080  pgnbgreunbgrlem4  48082  pgnbgreunbgrlem5lem1  48083  pgnbgreunbgrlem5lem2  48084  pgnbgreunbgrlem5lem3  48085  pgnbgreunbgrlem5  48086  0aryfvalel  48596  1arymaptf1  48604  2arymaptf1  48615  prelrrx2b  48676  rrx2xpref1o  48680  rrx2plordisom  48685  sectpropdlem  48998  ssccatid  49034  isthincd2lem2  49397