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  17615  catpropd  17650  funcsetcestrclem1  18095  symg2bas  19307  efgi  19633  gsumcom2  19889  pzriprnglem3  21425  pzriprnglem10  21432  mat1rhmval  22399  mat1ric  22407  txkgen  23572  cnmpt21  23591  xkoinjcn  23607  txconn  23609  xpstopnlem1  23729  qustgplem  24041  metustid  24475  axlowdim2  28940  axlowdim  28941  axcontlem2  28945  axcontlem3  28946  axcontlem4  28947  axcontlem9  28952  axcontlem10  28953  axcontlem11  28954  cusgrexg  29424  rgrusgrprc  29570  2clwwlk2clwwlk  30329  isnvlem  30589  br8d  32588  gsumhashmul  33044  prsdm  33897  eulerpartlemgvv  34360  reprsuc  34599  bnj941  34755  bnj944  34921  fineqvrep  35078  cvmlift2lem1  35282  cvmlift2lem12  35294  goel  35327  gonafv  35330  satf0op  35357  sat1el2xp  35359  fmla0xp  35363  sategoelfvb  35399  br8  35736  br6  35737  br4  35738  dfrn5  35754  elima4  35756  pprodss4v  35865  brimg  35918  brapply  35919  brsuccf  35922  brrestrict  35930  dfrdg4  35932  cgrtriv  35983  brofs  35986  segconeu  35992  btwntriv2  35993  transportprops  36015  brifs  36024  ifscgr  36025  brcgr3  36027  cgrxfr  36036  brcolinear2  36039  colineardim1  36042  brfs  36060  idinside  36065  btwnconn1lem7  36074  btwnconn1lem11  36078  btwnconn1lem12  36079  btwnconn1lem14  36081  brsegle  36089  seglerflx  36093  seglemin  36094  segleantisym  36096  btwnsegle  36098  outsideofeu  36112  outsidele  36113  linedegen  36124  fvline  36125  cbvoprab2vw  36219  cbvoprab23vw  36221  cbvopab2davw  36246  cbvoprab2davw  36253  finxpreclem6  37377  finxpsuclem  37378  curfv  37587  poimirlem4  37611  poimirlem26  37633  isdivrngo  37937  drngoi  37938  iss2  38319  dibelval3  41134  diblsmopel  41158  dihjatcclem4  41408  frlmsnic  42521  dfhe3  43757  dffrege115  43960  dropab2  44430  relopabVD  44883  projf1o  45184  sge0xp  46420  hoidmv1le  46585  fsetsniunop  47043  fsetsnf  47045  fsetsnf1  47046  fsetsnfo  47047  ichnreuop  47466  ichreuopeq  47467  reuopreuprim  47520  gpgprismgriedgdmss  48036  gpgvtx0  48037  gpgvtx1  48038  gpgedgvtx0  48045  gpgedgvtx1  48046  gpgedgiov  48049  gpgedg2ov  48050  gpgedg2iv  48051  gpg3kgrtriexlem6  48072  gpgprismgr4cycllem3  48080  pgnbgreunbgrlem1  48096  pgnbgreunbgrlem2  48100  pgnbgreunbgrlem4  48102  pgnbgreunbgrlem5lem1  48103  pgnbgreunbgrlem5lem2  48104  pgnbgreunbgrlem5lem3  48105  pgnbgreunbgrlem5  48106  0aryfvalel  48616  1arymaptf1  48624  2arymaptf1  48635  prelrrx2b  48696  rrx2xpref1o  48700  rrx2plordisom  48705  sectpropdlem  49018  ssccatid  49054  isthincd2lem2  49417