Theorem opeq2 4846

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 2852	. . . 4 ⊢ (𝐴 = 𝐵 → (𝐴 ∈ V ↔ 𝐵 ∈ V))
2	1	anbi2d 642	. . 3 ⊢ (𝐴 = 𝐵 → ((𝐶 ∈ V ∧ 𝐴 ∈ V) ↔ (𝐶 ∈ V ∧ 𝐵 ∈ V)))
3		preq2 4697	. . . 4 ⊢ (𝐴 = 𝐵 → {𝐶, 𝐴} = {𝐶, 𝐵})
4	3	preq2d 4703	. . 3 ⊢ (𝐴 = 𝐵 → {{𝐶}, {𝐶, 𝐴}} = {{𝐶}, {𝐶, 𝐵}})
5	2, 4	ifbieq1d 4510	. 2 ⊢ (𝐴 = 𝐵 → if((𝐶 ∈ V ∧ 𝐴 ∈ V), {{𝐶}, {𝐶, 𝐴}}, ∅) = if((𝐶 ∈ V ∧ 𝐵 ∈ V), {{𝐶}, {𝐶, 𝐵}}, ∅))
6		dfopif 4842	. 2 ⊢ ⟨𝐶, 𝐴⟩ = if((𝐶 ∈ V ∧ 𝐴 ∈ V), {{𝐶}, {𝐶, 𝐴}}, ∅)
7		dfopif 4842	. 2 ⊢ ⟨𝐶, 𝐵⟩ = if((𝐶 ∈ V ∧ 𝐵 ∈ V), {{𝐶}, {𝐶, 𝐵}}, ∅)
8	5, 6, 7	3eqtr4g 2823	1 ⊢ (𝐴 = 𝐵 → ⟨𝐶, 𝐴⟩ = ⟨𝐶, 𝐵⟩)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570   ∈ wcel 2147  Vcvv 3454  ∅c0 4281  ifcif 4485  {csn 4588  {cpr 4590  ⟨cop 4840

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4841

This theorem is used by:  opeq12  4847  opeq2i  4849  opeq2d  4852  oteq2  4866  oteq3  4867  breq2  5112  cbvopab2  5187  cbvopab2v  5190  opthg  5453  eqvinop  5463  opelopabsb  5511  dfid3  5556  opelxp  5694  relopabiOLD  5810  opabid2  5816  elrn2g  5884  opeldmd  5900  opeldm  5901  iss  6045  elidinxp  6054  dmsnopg  6233  reuop  6322  funopg  6602  f1osng  6898  f1oprswap  6901  tz6.12f  6941  fvn0ssdmfun  7106  fsn  7168  fsng  7170  fprg  7191  fprb  7230  oveq2  7459  cbvoprab2  7539  cbvoprab3v  7543  ovg  7617  elxp4  7968  elxp5  7969  opabex3d  8011  opabex3rd  8012  opabex3  8013  op1stg  8047  op2ndg  8048  op1steq  8079  dfoprab4f  8102  fsplit  8165  xpord2pred  8199  seqomlem2  8499  omeu  8631  oeeui  8649  curfv  8930  ralxpmap  8962  elixpsn  9003  ixpsnf1o  9004  mapsnend  9102  xpsnen  9118  xpassen  9128  xpf1o  9196  unxpdomlem1  9285  djulcl  10028  djurcl  10029  djur  10037  djuss  10038  djuun  10044  1stinl  10045  2ndinl  10046  1stinr  10047  2ndinr  10048  axdc4lem  10572  nqereu  11053  mulcanenq  11084  elreal  11255  ax1rid  11285  fseq1p1m1  13772  pfxval  14865  swrdccatin1  14916  swrdccat3blem  14930  wrdlen2  15138  ruclem1  16443  imasaddfnlem  17750  imasvscafn  17759  catidex  17898  catpropd  17933  funcsetcestrclem1  18378  degenmgm  19187  degenmgm2nfun  19189  degenmgm2  19190  symg2bas  19658  efgi  19984  gsumcom2  20240  pzriprnglem3  21844  pzriprnglem10  21851  mat1rhmval  22849  mat1ric  22857  txkgen  24026  cnmpt21  24045  xkoinjcn  24061  txconn  24063  xpstopnlem1  24183  qustgplem  24495  metustid  24928  angmgmval  29451  axlowdim2  29595  axlowdim  29596  axcontlem2  29600  axcontlem3  29601  axcontlem4  29602  axcontlem9  29607  axcontlem10  29608  axcontlem11  29609  cusgrexg  30082  rgrusgrprc  30227  2clwwlk2clwwlk  31008  isnvlem  31269  br8d  33300  gsumhashmul  33727  prsdm  34657  eulerpartlemgvv  35119  reprsuc  35355  bnj941  35514  bnj944  35679  omeueq  35837  soinfdom  35841  fineqvrep  35923  gdlopcfv1  36013  gdlopcfv2  36014  gdlopcfv3  36015  gdlopcfv4  36016  gdlopcfv5  36017  gdlopcfv6  36018  gdlopcfv7  36019  gdlopcfv8  36020  j00smo  36046  maxssj0  36047  j0le  36060  k3n0j0lt  36061  jltaleph  36067  cvmlift2lem1  36275  cvmlift2lem12  36287  goel  36320  gonafv  36323  satf0op  36350  sat1el2xp  36352  fmla0xp  36356  sategoelfvb  36392  br8  36736  br6  36737  br4  36738  dfrn5  36753  elima4  36755  pprodss4v  36861  brimg  36914  brapply  36915  lemsuccf  36918  brrestrict  36928  dfrdg4  36930  cgrtriv  36982  brofs  36985  segconeu  36991  btwntriv2  36992  transportprops  37014  brifs  37023  ifscgr  37024  brcgr3  37026  cgrxfr  37035  brcolinear2  37038  colineardim1  37041  brfs  37059  idinside  37064  btwnconn1lem7  37073  btwnconn1lem11  37077  btwnconn1lem12  37078  btwnconn1lem14  37080  brsegle  37088  seglerflx  37092  seglemin  37093  segleantisym  37095  btwnsegle  37097  outsideofeu  37111  outsidele  37112  linedegen  37123  fvline  37124  cbvoprab2vw  37242  cbvoprab23vw  37244  cbvopab2davw  37269  cbvoprab2davw  37276  finxpreclem6  38587  finxpsuclem  38588  poimirlem4  38810  poimirlem26  38832  isdivrngo  39150  drngoi  39151  iss2  39542  dibelval3  42470  diblsmopel  42494  dihjatcclem4  42744  frlmsnic  43870  dfhe3  45036  dffrege115  45239  dropab2  45691  relopabVD  46143  projf1o  46484  sge0xp  47712  hoidmv1le  47877  fsetsniunop  48392  fsetsnf  48394  fsetsnf1  48395  fsetsnfo  48396  ichnreuop  48827  ichreuopeq  48828  reuopreuprim  48881  gpgprismgriedgdmss  49423  gpgvtx0  49424  gpgvtx1  49425  gpgedgvtx0  49432  gpgedgvtx1  49433  gpgedgiov  49436  gpgedg2ov  49437  gpgedg2iv  49438  gpg3kgrtriexlem6  49459  gpgprismgr4cycllem3  49468  pgnbgreunbgrlem1  49484  pgnbgreunbgrlem2  49488  pgnbgreunbgrlem4  49490  pgnbgreunbgrlem5lem1  49491  pgnbgreunbgrlem5lem2  49492  pgnbgreunbgrlem5lem3  49493  pgnbgreunbgrlem5  49494  gpg5edgnedg  49501  0aryfvalel  50077  1arymaptf1  50085  2arymaptf1  50096  sectpropdlem  50481  ssccatid  50517  isthincd2lem2  50901  fuconuniqex2  51118