Theorem opeq2 4832

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 2850	. . . 4 ⊢ (𝐴 = 𝐵 → (𝐴 ∈ V ↔ 𝐵 ∈ V))
2	1	anbi2d 639	. . 3 ⊢ (𝐴 = 𝐵 → ((𝐶 ∈ V ∧ 𝐴 ∈ V) ↔ (𝐶 ∈ V ∧ 𝐵 ∈ V)))
3		preq2 4693	. . . 4 ⊢ (𝐴 = 𝐵 → {𝐶, 𝐴} = {𝐶, 𝐵})
4	3	preq2d 4699	. . 3 ⊢ (𝐴 = 𝐵 → {{𝐶}, {𝐶, 𝐴}} = {{𝐶}, {𝐶, 𝐵}})
5	2, 4	ifbieq1d 4505	. 2 ⊢ (𝐴 = 𝐵 → if((𝐶 ∈ V ∧ 𝐴 ∈ V), {{𝐶}, {𝐶, 𝐴}}, ∅) = if((𝐶 ∈ V ∧ 𝐵 ∈ V), {{𝐶}, {𝐶, 𝐵}}, ∅))
6		dfopif 4828	. 2 ⊢ ⟨𝐶, 𝐴⟩ = if((𝐶 ∈ V ∧ 𝐴 ∈ V), {{𝐶}, {𝐶, 𝐴}}, ∅)
7		dfopif 4828	. 2 ⊢ ⟨𝐶, 𝐵⟩ = if((𝐶 ∈ V ∧ 𝐵 ∈ V), {{𝐶}, {𝐶, 𝐵}}, ∅)
8	5, 6, 7	3eqtr4g 2822	1 ⊢ (𝐴 = 𝐵 → ⟨𝐶, 𝐴⟩ = ⟨𝐶, 𝐵⟩)

Syntax hints:   → wi 4   ∧ wa 399   = wceq 1560   ∈ wcel 2142  Vcvv 3454  ∅c0 4285  ifcif 4480  {csn 4582  {cpr 4584  ⟨cop 4588

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1100  df-tru 1563  df-fal 1573  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-rab 3415  df-v 3456  df-dif 3907  df-un 3909  df-ss 3921  df-nul 4286  df-if 4481  df-sn 4583  df-pr 4585  df-op 4589

This theorem is referenced by:  opeq12  4833  opeq2i  4835  opeq2d  4838  oteq2  4841  oteq3  4842  breq2  5104  cbvopab2  5176  cbvopab2v  5179  opthg  5445  eqvinop  5455  opelopabsb  5500  dfid3  5545  opelxp  5683  relopabi  5795  opabid2  5801  elrn2g  5866  opeldmd  5882  opeldm  5883  iss  6024  elidinxp  6033  dmsnopg  6200  reuop  6280  funopg  6555  f1osng  6849  f1oprswap  6852  tz6.12f  6892  fvn0ssdmfun  7055  fsn  7117  fsng  7119  fprg  7138  fprb  7178  oveq2  7404  cbvoprab2  7484  cbvoprab3v  7488  ovg  7561  elxp4  7903  elxp5  7904  opabex3d  7946  opabex3rd  7947  opabex3  7948  op1stg  7982  op2ndg  7983  op1steq  8014  dfoprab4f  8037  fsplit  8096  xpord2pred  8125  seqomlem2  8422  omeu  8554  oeeui  8572  ralxpmap  8878  elixpsn  8919  ixpsnf1o  8920  mapsnend  9017  xpsnen  9033  xpassen  9043  xpf1o  9111  unxpdomlem1  9200  djulcl  9868  djurcl  9869  djur  9877  djuss  9878  djuun  9884  1stinl  9885  2ndinl  9886  1stinr  9887  2ndinr  9888  axdc4lem  10412  nqereu  10887  mulcanenq  10918  elreal  11089  ax1rid  11119  fseq1p1m1  13603  pfxval  14687  swrdccatin1  14738  swrdccat3blem  14752  wrdlen2  14957  ruclem1  16263  imasaddfnlem  17558  imasvscafn  17567  catidex  17706  catpropd  17741  funcsetcestrclem1  18186  symg2bas  19433  efgi  19759  gsumcom2  20015  pzriprnglem3  21532  pzriprnglem10  21539  mat1rhmval  22536  mat1ric  22544  txkgen  23709  cnmpt21  23728  xkoinjcn  23744  txconn  23746  xpstopnlem1  23866  qustgplem  24178  metustid  24611  axlowdim2  29158  axlowdim  29159  axcontlem2  29163  axcontlem3  29164  axcontlem4  29165  axcontlem9  29170  axcontlem10  29171  axcontlem11  29172  cusgrexg  29642  rgrusgrprc  29787  2clwwlk2clwwlk  30549  isnvlem  30810  br8d  32807  gsumhashmul  33244  prsdm  34208  eulerpartlemgvv  34670  reprsuc  34906  bnj941  35065  bnj944  35230  fineqvrep  35407  cvmlift2lem1  35649  cvmlift2lem12  35661  goel  35694  gonafv  35697  satf0op  35724  sat1el2xp  35726  fmla0xp  35730  sategoelfvb  35766  br8  36103  br6  36104  br4  36105  dfrn5  36121  elima4  36123  pprodss4v  36229  brimg  36282  brapply  36283  lemsuccf  36286  brrestrict  36296  dfrdg4  36298  cgrtriv  36349  brofs  36352  segconeu  36358  btwntriv2  36359  transportprops  36381  brifs  36390  ifscgr  36391  brcgr3  36393  cgrxfr  36402  brcolinear2  36405  colineardim1  36408  brfs  36426  idinside  36431  btwnconn1lem7  36440  btwnconn1lem11  36444  btwnconn1lem12  36445  btwnconn1lem14  36447  brsegle  36455  seglerflx  36459  seglemin  36460  segleantisym  36462  btwnsegle  36464  outsideofeu  36478  outsidele  36479  linedegen  36490  fvline  36491  cbvoprab2vw  36595  cbvoprab23vw  36597  cbvopab2davw  36622  cbvoprab2davw  36629  finxpreclem6  37887  finxpsuclem  37888  curfv  38096  poimirlem4  38120  poimirlem26  38142  isdivrngo  38446  drngoi  38447  iss2  38840  dibelval3  41768  diblsmopel  41792  dihjatcclem4  42042  frlmsnic  43155  dfhe3  44348  dffrege115  44551  dropab2  45020  relopabVD  45473  projf1o  45771  sge0xp  47000  hoidmv1le  47165  fsetsniunop  47640  fsetsnf  47642  fsetsnf1  47643  fsetsnfo  47644  ichnreuop  48075  ichreuopeq  48076  reuopreuprim  48129  gpgprismgriedgdmss  48671  gpgvtx0  48672  gpgvtx1  48673  gpgedgvtx0  48680  gpgedgvtx1  48681  gpgedgiov  48684  gpgedg2ov  48685  gpgedg2iv  48686  gpg3kgrtriexlem6  48707  gpgprismgr4cycllem3  48716  pgnbgreunbgrlem1  48732  pgnbgreunbgrlem2  48736  pgnbgreunbgrlem4  48738  pgnbgreunbgrlem5lem1  48739  pgnbgreunbgrlem5lem2  48740  pgnbgreunbgrlem5lem3  48741  pgnbgreunbgrlem5  48742  gpg5edgnedg  48749  0aryfvalel  49253  1arymaptf1  49261  2arymaptf1  49272  prelrrx2b  49333  rrx2xpref1o  49337  rrx2plordisom  49342  sectpropdlem  49654  ssccatid  49690  isthincd2lem2  50053