Theorem opeq2 4341

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 2676	. . . 4 ⊢ (𝐴 = 𝐵 → (𝐴 ∈ V ↔ 𝐵 ∈ V))
2	1	anbi2d 736	. . 3 ⊢ (𝐴 = 𝐵 → ((𝐶 ∈ V ∧ 𝐴 ∈ V) ↔ (𝐶 ∈ V ∧ 𝐵 ∈ V)))
3		preq2 4213	. . . 4 ⊢ (𝐴 = 𝐵 → {𝐶, 𝐴} = {𝐶, 𝐵})
4	3	preq2d 4219	. . 3 ⊢ (𝐴 = 𝐵 → {{𝐶}, {𝐶, 𝐴}} = {{𝐶}, {𝐶, 𝐵}})
5	2, 4	ifbieq1d 4059	. 2 ⊢ (𝐴 = 𝐵 → if((𝐶 ∈ V ∧ 𝐴 ∈ V), {{𝐶}, {𝐶, 𝐴}}, ∅) = if((𝐶 ∈ V ∧ 𝐵 ∈ V), {{𝐶}, {𝐶, 𝐵}}, ∅))
6		dfopif 4337	. 2 ⊢ ⟨𝐶, 𝐴⟩ = if((𝐶 ∈ V ∧ 𝐴 ∈ V), {{𝐶}, {𝐶, 𝐴}}, ∅)
7		dfopif 4337	. 2 ⊢ ⟨𝐶, 𝐵⟩ = if((𝐶 ∈ V ∧ 𝐵 ∈ V), {{𝐶}, {𝐶, 𝐵}}, ∅)
8	5, 6, 7	3eqtr4g 2669	1 ⊢ (𝐴 = 𝐵 → ⟨𝐶, 𝐴⟩ = ⟨𝐶, 𝐵⟩)

Syntax hints:   → wi 4   ∧ wa 383   = wceq 1475   ∈ wcel 1977  Vcvv 3173  ∅c0 3874  ifcif 4036  {csn 4125  {cpr 4127  ⟨cop 4131

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-rab 2905  df-v 3175  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132

This theorem is referenced by:  opeq12  4342  opeq2i  4344  opeq2d  4347  oteq2  4350  oteq3  4351  breq2  4587  cbvopab2  4656  cbvopab2v  4659  opthg  4872  eqvinop  4881  opelopabsb  4910  dfid3  4954  opelxp  5070  relopabi  5167  opabid2  5173  elrn2g  5235  opeldmd  5249  opeldm  5250  elrn2  5286  opelresg  5324  iss  5367  elimasng  5410  issref  5428  dmsnopg  5524  cnvsng  5539  funopg  5836  f1osng  6089  f1oprswap  6092  tz6.12f  6122  fvn0ssdmfun  6258  fsn  6308  fsng  6310  funsneqopsn  6322  fprg  6327  fvsng  6352  oveq2  6557  cbvoprab2  6626  ovg  6697  elxp4  7003  elxp5  7004  opabex3d  7037  opabex3  7038  op1stg  7071  op2ndg  7072  op1steq  7101  dfoprab4f  7117  seqomlem2  7433  omeu  7552  oeeui  7569  ralxpmap  7793  elixpsn  7833  ixpsnf1o  7834  mapsnen  7920  xpsnen  7929  xpassen  7939  xpf1o  8007  unxpdomlem1  8049  axdc4lem  9160  nqereu  9630  mulcanenq  9661  elreal  9831  ax1rid  9861  fseq1p1m1  12283  swrdccatin1  13334  swrdccat3blem  13346  swrdccatid  13348  swrdccatin12d  13352  wrdlen2  13536  ruclem1  14799  imasaddfnlem  16011  imasvscafn  16020  catidex  16158  catpropd  16192  funcsetcestrclem1  16617  symg2bas  17641  psgnunilem5  17737  efgi  17955  gsumcom2  18197  mat1rhmval  20104  mat1ric  20112  txkgen  21265  cnmpt21  21284  xkoinjcn  21300  txcon  21302  xpstopnlem1  21422  qustgplem  21734  metustid  22169  axlowdim2  25640  axlowdim  25641  axcontlem2  25645  axcontlem3  25646  axcontlem4  25647  axcontlem9  25652  axcontlem10  25653  axcontlem11  25654  1pthoncl  26122  2pthoncl  26133  wwlknextbi  26253  wwlkextinj  26258  wwlkextsur  26259  clwwlkfo  26325  0eusgraiff0rgra  26466  isnvlem  26849  br8d  28802  prsdm  29288  eulerpartlemgvv  29765  bnj941  30097  bnj944  30262  cvmlift2lem1  30538  cvmlift2lem12  30550  br8  30899  br6  30900  br4  30901  fprb  30916  br1steqg  30919  br2ndeqg  30920  dfrn5  30922  elima4  30924  pprodss4v  31161  brimg  31214  brapply  31215  brsuccf  31218  brrestrict  31226  dfrdg4  31228  cgrtriv  31279  brofs  31282  segconeu  31288  btwntriv2  31289  transportprops  31311  brifs  31320  ifscgr  31321  brcgr3  31323  cgrxfr  31332  brcolinear2  31335  colineardim1  31338  brfs  31356  idinside  31361  btwnconn1lem7  31370  btwnconn1lem11  31374  btwnconn1lem12  31375  btwnconn1lem14  31377  brsegle  31385  seglerflx  31389  seglemin  31390  segleantisym  31392  btwnsegle  31394  outsideofeu  31408  outsidele  31409  linedegen  31420  fvline  31421  finxpreclem6  32409  finxpsuclem  32410  curfv  32559  poimirlem4  32583  poimirlem26  32605  isdivrngo  32919  drngoi  32920  dibelval3  35454  diblsmopel  35478  dihjatcclem4  35728  dfhe3  37089  dffrege115  37292  dropab2  37673  relopabVD  38159  projf1o  38381  mapsnend  38386  sge0xp  39322  hoidmv1le  39484  pfxval  40246  cusgrexg  40663  rgrusgrprc  40789  wwlksnextbi  41100  wwlksnextinj  41105  wwlksnextsur  41106  clwwlksfo  41225  clwlksfclwwlk  41269