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 2849	. . . 4 ⊢ (𝐴 = 𝐵 → (𝐴 ∈ V ↔ 𝐵 ∈ V))
2	1	anbi2d 642	. . 3 ⊢ (𝐴 = 𝐵 → ((𝐶 ∈ V ∧ 𝐴 ∈ V) ↔ (𝐶 ∈ V ∧ 𝐵 ∈ V)))
3		preq2 4695	. . . 4 ⊢ (𝐴 = 𝐵 → {𝐶, 𝐴} = {𝐶, 𝐵})
4	3	preq2d 4701	. . 3 ⊢ (𝐴 = 𝐵 → {{𝐶}, {𝐶, 𝐴}} = {{𝐶}, {𝐶, 𝐵}})
5	2, 4	ifbieq1d 4507	. 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 2821	1 ⊢ (𝐴 = 𝐵 → ⟨𝐶, 𝐴⟩ = ⟨𝐶, 𝐵⟩)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570   ∈ wcel 2145  Vcvv 3451  ∅c0 4279  ifcif 4482  {csn 4584  {cpr 4586  ⟨cop 4590

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 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

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 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591

This theorem is used by:  opeq12  4835  opeq2i  4837  opeq2d  4840  oteq2  4843  oteq3  4844  breq2  5107  cbvopab2  5181  cbvopab2v  5184  opthg  5446  eqvinop  5456  opelopabsb  5504  dfid3  5549  opelxp  5687  relopabi  5800  opabid2  5806  elrn2g  5872  opeldmd  5888  opeldm  5889  iss  6027  elidinxp  6036  dmsnopg  6213  reuop  6295  funopg  6572  f1osng  6865  f1oprswap  6868  tz6.12f  6908  fvn0ssdmfun  7072  fsn  7134  fsng  7136  fprg  7157  fprb  7197  oveq2  7426  cbvoprab2  7506  cbvoprab3v  7510  ovg  7583  elxp4  7932  elxp5  7933  opabex3d  7975  opabex3rd  7976  opabex3  7977  op1stg  8011  op2ndg  8012  op1steq  8043  dfoprab4f  8065  fsplit  8126  xpord2pred  8155  seqomlem2  8454  omeu  8586  oeeui  8604  curfv  8885  ralxpmap  8917  elixpsn  8958  ixpsnf1o  8959  mapsnend  9057  xpsnen  9073  xpassen  9083  xpf1o  9151  unxpdomlem1  9240  djulcl  9984  djurcl  9985  djur  9993  djuss  9994  djuun  10000  1stinl  10001  2ndinl  10002  1stinr  10003  2ndinr  10004  axdc4lem  10526  nqereu  11007  mulcanenq  11038  elreal  11209  ax1rid  11239  fseq1p1m1  13725  pfxval  14816  swrdccatin1  14867  swrdccat3blem  14881  wrdlen2  15088  ruclem1  16392  imasaddfnlem  17693  imasvscafn  17702  catidex  17841  catpropd  17876  funcsetcestrclem1  18321  degenmgm  19130  degenmgm2nfun  19132  degenmgm2  19133  symg2bas  19600  efgi  19926  gsumcom2  20182  pzriprnglem3  21782  pzriprnglem10  21789  mat1rhmval  22787  mat1ric  22795  txkgen  23964  cnmpt21  23983  xkoinjcn  23999  txconn  24001  xpstopnlem1  24121  qustgplem  24433  metustid  24866  angmgmval  29387  axlowdim2  29531  axlowdim  29532  axcontlem2  29536  axcontlem3  29537  axcontlem4  29538  axcontlem9  29543  axcontlem10  29544  axcontlem11  29545  cusgrexg  30018  rgrusgrprc  30163  2clwwlk2clwwlk  30944  isnvlem  31205  br8d  33195  gsumhashmul  33621  prsdm  34539  eulerpartlemgvv  35001  reprsuc  35237  bnj941  35396  bnj944  35561  fineqvrep  35765  cvmlift2lem1  36046  cvmlift2lem12  36058  goel  36091  gonafv  36094  satf0op  36121  sat1el2xp  36123  fmla0xp  36127  sategoelfvb  36163  br8  36500  br6  36501  br4  36502  dfrn5  36518  elima4  36520  pprodss4v  36626  brimg  36679  brapply  36680  lemsuccf  36683  brrestrict  36693  dfrdg4  36695  cgrtriv  36747  brofs  36750  segconeu  36756  btwntriv2  36757  transportprops  36779  brifs  36788  ifscgr  36789  brcgr3  36791  cgrxfr  36800  brcolinear2  36803  colineardim1  36806  brfs  36824  idinside  36829  btwnconn1lem7  36838  btwnconn1lem11  36842  btwnconn1lem12  36843  btwnconn1lem14  36845  brsegle  36853  seglerflx  36857  seglemin  36858  segleantisym  36860  btwnsegle  36862  outsideofeu  36876  outsidele  36877  linedegen  36888  fvline  36889  cbvoprab2vw  37007  cbvoprab23vw  37009  cbvopab2davw  37034  cbvoprab2davw  37041  finxpreclem6  38299  finxpsuclem  38300  poimirlem4  38522  poimirlem26  38544  isdivrngo  38864  drngoi  38865  iss2  39256  dibelval3  42184  diblsmopel  42208  dihjatcclem4  42458  frlmsnic  43584  dfhe3  44760  dffrege115  44963  dropab2  45416  relopabVD  45868  projf1o  46180  sge0xp  47408  hoidmv1le  47573  fsetsniunop  48088  fsetsnf  48090  fsetsnf1  48091  fsetsnfo  48092  ichnreuop  48523  ichreuopeq  48524  reuopreuprim  48577  gpgprismgriedgdmss  49119  gpgvtx0  49120  gpgvtx1  49121  gpgedgvtx0  49128  gpgedgvtx1  49129  gpgedgiov  49132  gpgedg2ov  49133  gpgedg2iv  49134  gpg3kgrtriexlem6  49155  gpgprismgr4cycllem3  49164  pgnbgreunbgrlem1  49180  pgnbgreunbgrlem2  49184  pgnbgreunbgrlem4  49186  pgnbgreunbgrlem5lem1  49187  pgnbgreunbgrlem5lem2  49188  pgnbgreunbgrlem5lem3  49189  pgnbgreunbgrlem5  49190  gpg5edgnedg  49197  0aryfvalel  49715  1arymaptf1  49723  2arymaptf1  49734  prelrrx2b  49795  rrx2xpref1o  49799  rrx2plordisom  49804  sectpropdlem  50113  ssccatid  50149  isthincd2lem2  50512