Theorem opeq2 4828

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 2822	. . . 4 ⊢ (𝐴 = 𝐵 → (𝐴 ∈ V ↔ 𝐵 ∈ V))
2	1	anbi2d 630	. . 3 ⊢ (𝐴 = 𝐵 → ((𝐶 ∈ V ∧ 𝐴 ∈ V) ↔ (𝐶 ∈ V ∧ 𝐵 ∈ V)))
3		preq2 4689	. . . 4 ⊢ (𝐴 = 𝐵 → {𝐶, 𝐴} = {𝐶, 𝐵})
4	3	preq2d 4695	. . 3 ⊢ (𝐴 = 𝐵 → {{𝐶}, {𝐶, 𝐴}} = {{𝐶}, {𝐶, 𝐵}})
5	2, 4	ifbieq1d 4502	. 2 ⊢ (𝐴 = 𝐵 → if((𝐶 ∈ V ∧ 𝐴 ∈ V), {{𝐶}, {𝐶, 𝐴}}, ∅) = if((𝐶 ∈ V ∧ 𝐵 ∈ V), {{𝐶}, {𝐶, 𝐵}}, ∅))
6		dfopif 4824	. 2 ⊢ ⟨𝐶, 𝐴⟩ = if((𝐶 ∈ V ∧ 𝐴 ∈ V), {{𝐶}, {𝐶, 𝐴}}, ∅)
7		dfopif 4824	. 2 ⊢ ⟨𝐶, 𝐵⟩ = if((𝐶 ∈ V ∧ 𝐵 ∈ V), {{𝐶}, {𝐶, 𝐵}}, ∅)
8	5, 6, 7	3eqtr4g 2794	1 ⊢ (𝐴 = 𝐵 → ⟨𝐶, 𝐴⟩ = ⟨𝐶, 𝐵⟩)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1541   ∈ wcel 2113  Vcvv 3438  ∅c0 4283  ifcif 4477  {csn 4578  {cpr 4580  ⟨cop 4584

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-rab 3398  df-v 3440  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4284  df-if 4478  df-sn 4579  df-pr 4581  df-op 4585

This theorem is referenced by:  opeq12  4829  opeq2i  4831  opeq2d  4834  oteq2  4837  oteq3  4838  breq2  5100  cbvopab2  5172  cbvopab2v  5175  opthg  5423  eqvinop  5433  opelopabsb  5476  dfid3  5520  opelxp  5658  relopabi  5769  opabid2  5775  elrn2g  5837  opeldmd  5853  opeldm  5854  iss  5992  elidinxp  6001  dmsnopg  6169  reuop  6249  funopg  6524  f1osng  6814  f1oprswap  6817  tz6.12f  6857  fvn0ssdmfun  7017  fsn  7078  fsng  7080  fprg  7098  fprb  7138  oveq2  7364  cbvoprab2  7444  cbvoprab3v  7448  ovg  7521  elxp4  7862  elxp5  7863  opabex3d  7907  opabex3rd  7908  opabex3  7909  op1stg  7943  op2ndg  7944  op1steq  7975  dfoprab4f  7998  fsplit  8057  xpord2pred  8085  seqomlem2  8380  omeu  8510  oeeui  8528  ralxpmap  8832  elixpsn  8873  ixpsnf1o  8874  mapsnend  8971  xpsnen  8987  xpassen  8997  xpf1o  9065  unxpdomlem1  9154  djulcl  9820  djurcl  9821  djur  9829  djuss  9830  djuun  9836  1stinl  9837  2ndinl  9838  1stinr  9839  2ndinr  9840  axdc4lem  10363  nqereu  10838  mulcanenq  10869  elreal  11040  ax1rid  11070  fseq1p1m1  13512  pfxval  14595  swrdccatin1  14646  swrdccat3blem  14660  wrdlen2  14865  ruclem1  16154  imasaddfnlem  17447  imasvscafn  17456  catidex  17595  catpropd  17630  funcsetcestrclem1  18075  symg2bas  19320  efgi  19646  gsumcom2  19902  pzriprnglem3  21436  pzriprnglem10  21443  mat1rhmval  22421  mat1ric  22429  txkgen  23594  cnmpt21  23613  xkoinjcn  23629  txconn  23631  xpstopnlem1  23751  qustgplem  24063  metustid  24496  axlowdim2  28982  axlowdim  28983  axcontlem2  28987  axcontlem3  28988  axcontlem4  28989  axcontlem9  28994  axcontlem10  28995  axcontlem11  28996  cusgrexg  29466  rgrusgrprc  29612  2clwwlk2clwwlk  30374  isnvlem  30634  br8d  32635  gsumhashmul  33099  prsdm  34020  eulerpartlemgvv  34482  reprsuc  34721  bnj941  34877  bnj944  35043  fineqvrep  35219  cvmlift2lem1  35445  cvmlift2lem12  35457  goel  35490  gonafv  35493  satf0op  35520  sat1el2xp  35522  fmla0xp  35526  sategoelfvb  35562  br8  35899  br6  35900  br4  35901  dfrn5  35917  elima4  35919  pprodss4v  36025  brimg  36078  brapply  36079  lemsuccf  36082  brrestrict  36092  dfrdg4  36094  cgrtriv  36145  brofs  36148  segconeu  36154  btwntriv2  36155  transportprops  36177  brifs  36186  ifscgr  36187  brcgr3  36189  cgrxfr  36198  brcolinear2  36201  colineardim1  36204  brfs  36222  idinside  36227  btwnconn1lem7  36236  btwnconn1lem11  36240  btwnconn1lem12  36241  btwnconn1lem14  36243  brsegle  36251  seglerflx  36255  seglemin  36256  segleantisym  36258  btwnsegle  36260  outsideofeu  36274  outsidele  36275  linedegen  36286  fvline  36287  cbvoprab2vw  36381  cbvoprab23vw  36383  cbvopab2davw  36408  cbvoprab2davw  36415  finxpreclem6  37540  finxpsuclem  37541  curfv  37740  poimirlem4  37764  poimirlem26  37786  isdivrngo  38090  drngoi  38091  iss2  38476  dibelval3  41346  diblsmopel  41370  dihjatcclem4  41620  frlmsnic  42737  dfhe3  43958  dffrege115  44161  dropab2  44630  relopabVD  45083  projf1o  45383  sge0xp  46615  hoidmv1le  46780  fsetsniunop  47237  fsetsnf  47239  fsetsnf1  47240  fsetsnfo  47241  ichnreuop  47660  ichreuopeq  47661  reuopreuprim  47714  gpgprismgriedgdmss  48240  gpgvtx0  48241  gpgvtx1  48242  gpgedgvtx0  48249  gpgedgvtx1  48250  gpgedgiov  48253  gpgedg2ov  48254  gpgedg2iv  48255  gpg3kgrtriexlem6  48276  gpgprismgr4cycllem3  48285  pgnbgreunbgrlem1  48301  pgnbgreunbgrlem2  48305  pgnbgreunbgrlem4  48307  pgnbgreunbgrlem5lem1  48308  pgnbgreunbgrlem5lem2  48309  pgnbgreunbgrlem5lem3  48310  pgnbgreunbgrlem5  48311  gpg5edgnedg  48318  0aryfvalel  48822  1arymaptf1  48830  2arymaptf1  48841  prelrrx2b  48902  rrx2xpref1o  48906  rrx2plordisom  48911  sectpropdlem  49223  ssccatid  49259  isthincd2lem2  49622