Theorem opeq2 4637

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 2847	. . . 4 ⊢ (𝐴 = 𝐵 → (𝐴 ∈ V ↔ 𝐵 ∈ V))
2	1	anbi2d 622	. . 3 ⊢ (𝐴 = 𝐵 → ((𝐶 ∈ V ∧ 𝐴 ∈ V) ↔ (𝐶 ∈ V ∧ 𝐵 ∈ V)))
3		preq2 4501	. . . 4 ⊢ (𝐴 = 𝐵 → {𝐶, 𝐴} = {𝐶, 𝐵})
4	3	preq2d 4507	. . 3 ⊢ (𝐴 = 𝐵 → {{𝐶}, {𝐶, 𝐴}} = {{𝐶}, {𝐶, 𝐵}})
5	2, 4	ifbieq1d 4330	. 2 ⊢ (𝐴 = 𝐵 → if((𝐶 ∈ V ∧ 𝐴 ∈ V), {{𝐶}, {𝐶, 𝐴}}, ∅) = if((𝐶 ∈ V ∧ 𝐵 ∈ V), {{𝐶}, {𝐶, 𝐵}}, ∅))
6		dfopif 4633	. 2 ⊢ ⟨𝐶, 𝐴⟩ = if((𝐶 ∈ V ∧ 𝐴 ∈ V), {{𝐶}, {𝐶, 𝐴}}, ∅)
7		dfopif 4633	. 2 ⊢ ⟨𝐶, 𝐵⟩ = if((𝐶 ∈ V ∧ 𝐵 ∈ V), {{𝐶}, {𝐶, 𝐵}}, ∅)
8	5, 6, 7	3eqtr4g 2839	1 ⊢ (𝐴 = 𝐵 → ⟨𝐶, 𝐴⟩ = ⟨𝐶, 𝐵⟩)

Syntax hints:   → wi 4   ∧ wa 386   = wceq 1601   ∈ wcel 2107  Vcvv 3398  ∅c0 4141  ifcif 4307  {csn 4398  {cpr 4400  ⟨cop 4404

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-13 2334  ax-ext 2754

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3an 1073  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-rab 3099  df-v 3400  df-dif 3795  df-un 3797  df-in 3799  df-ss 3806  df-nul 4142  df-if 4308  df-sn 4399  df-pr 4401  df-op 4405

This theorem is referenced by:  opeq12  4638  opeq2i  4640  opeq2d  4643  oteq2  4646  oteq3  4647  breq2  4890  cbvopab2  4960  cbvopab2v  4963  opthg  5177  eqvinop  5186  opelopabsb  5222  dfid3  5262  opelxp  5391  relopabi  5491  opabid2  5497  elrn2g  5558  opeldmd  5572  opeldm  5573  elrn2  5611  iss  5697  elidinxp  5705  elridOLD  5708  elimasng  5745  idrefOLD  5764  dmsnopg  5860  funopg  6169  f1osng  6431  f1oprswap  6434  tz6.12f  6470  fvn0ssdmfun  6614  fsn  6667  fsng  6669  funsneqopsnOLD  6683  fprg  6688  fvsngOLD  6716  fprb  6731  oveq2  6930  cbvoprab2  7005  ovg  7076  elxp4  7389  elxp5  7390  opabex3d  7423  opabex3  7424  op1stg  7457  op2ndg  7458  op1steq  7489  dfoprab4f  7505  seqomlem2  7829  omeu  7949  oeeui  7966  ralxpmap  8193  elixpsn  8233  ixpsnf1o  8234  mapsnend  8320  xpsnen  8332  xpassen  8342  xpf1o  8410  unxpdomlem1  8452  djulcl  9069  djurcl  9070  djur  9078  djuss  9079  djuun  9085  1stinl  9086  2ndinl  9087  1stinr  9088  2ndinr  9089  axdc4lem  9612  nqereu  10086  mulcanenq  10117  elreal  10288  ax1rid  10318  fseq1p1m1  12732  pfxval  13782  swrdccatin1  13851  swrdccat3blem  13871  swrdccatidOLD  13875  swrdccatin12dOLD  13881  wrdlen2  14095  ruclem1  15364  imasaddfnlem  16574  imasvscafn  16583  catidex  16720  catpropd  16754  funcsetcestrclem1  17180  symg2bas  18201  psgnunilem5OLD  18298  efgi  18516  gsumcom2  18760  mat1rhmval  20690  mat1ric  20698  txkgen  21864  cnmpt21  21883  xkoinjcn  21899  txconn  21901  xpstopnlem1  22021  qustgplem  22332  metustid  22767  axlowdim2  26309  axlowdim  26310  axcontlem2  26314  axcontlem3  26315  axcontlem4  26316  axcontlem9  26321  axcontlem10  26322  axcontlem11  26323  cusgrexg  26792  rgrusgrprc  26937  wwlksnextbiOLD  27256  wwlksnextinjOLD  27268  wwlksnextsurOLD  27269  clwwlkfoOLD  27441  2clwwlk2clwwlk  27761  2clwwlk2clwwlkOLD  27762  isnvlem  28037  br8d  29985  prsdm  30558  eulerpartlemgvv  31036  reprsuc  31295  bnj941  31442  bnj944  31607  cvmlift2lem1  31883  cvmlift2lem12  31895  br8  32240  br6  32241  br4  32242  dfrn5  32265  elima4  32267  pprodss4v  32580  brimg  32633  brapply  32634  brsuccf  32637  brrestrict  32645  dfrdg4  32647  cgrtriv  32698  brofs  32701  segconeu  32707  btwntriv2  32708  transportprops  32730  brifs  32739  ifscgr  32740  brcgr3  32742  cgrxfr  32751  brcolinear2  32754  colineardim1  32757  brfs  32775  idinside  32780  btwnconn1lem7  32789  btwnconn1lem11  32793  btwnconn1lem12  32794  btwnconn1lem14  32796  brsegle  32804  seglerflx  32808  seglemin  32809  segleantisym  32811  btwnsegle  32813  outsideofeu  32827  outsidele  32828  linedegen  32839  fvline  32840  finxpreclem6  33828  finxpsuclem  33829  curfv  34014  poimirlem4  34039  poimirlem26  34061  isdivrngo  34373  drngoi  34374  iss2  34740  dibelval3  37301  diblsmopel  37325  dihjatcclem4  37575  dfhe3  39025  dffrege115  39228  dropab2  39606  relopabVD  40070  projf1o  40309  sge0xp  41570  hoidmv1le  41735  prelrrx2b  43450  rrx2xpref1o  43454  rrx2plordisom  43459