Theorem opeq1 4840

Description: Equality theorem for ordered pairs. (Contributed by NM, 25-Jun-1998.) (Revised by Mario Carneiro, 26-Apr-2015.)

Assertion

Ref	Expression
opeq1	⊢ (𝐴 = 𝐵 → ⟨𝐴, 𝐶⟩ = ⟨𝐵, 𝐶⟩)

Proof of Theorem opeq1

Step	Hyp	Ref	Expression
1		eleq1 2853	. . . 4 ⊢ (𝐴 = 𝐵 → (𝐴 ∈ V ↔ 𝐵 ∈ V))
2	1	anbi1d 643	. . 3 ⊢ (𝐴 = 𝐵 → ((𝐴 ∈ V ∧ 𝐶 ∈ V) ↔ (𝐵 ∈ V ∧ 𝐶 ∈ V)))
3		sneq 4601	. . . 4 ⊢ (𝐴 = 𝐵 → {𝐴} = {𝐵})
4		preq1 4701	. . . 4 ⊢ (𝐴 = 𝐵 → {𝐴, 𝐶} = {𝐵, 𝐶})
5	3, 4	preq12d 4709	. . 3 ⊢ (𝐴 = 𝐵 → {{𝐴}, {𝐴, 𝐶}} = {{𝐵}, {𝐵, 𝐶}})
6	2, 5	ifbieq1d 4514	. 2 ⊢ (𝐴 = 𝐵 → if((𝐴 ∈ V ∧ 𝐶 ∈ V), {{𝐴}, {𝐴, 𝐶}}, ∅) = if((𝐵 ∈ V ∧ 𝐶 ∈ V), {{𝐵}, {𝐵, 𝐶}}, ∅))
7		dfopif 4837	. 2 ⊢ ⟨𝐴, 𝐶⟩ = if((𝐴 ∈ V ∧ 𝐶 ∈ V), {{𝐴}, {𝐴, 𝐶}}, ∅)
8		dfopif 4837	. 2 ⊢ ⟨𝐵, 𝐶⟩ = if((𝐵 ∈ V ∧ 𝐶 ∈ V), {{𝐵}, {𝐵, 𝐶}}, ∅)
9	6, 7, 8	3eqtr4g 2825	1 ⊢ (𝐴 = 𝐵 → ⟨𝐴, 𝐶⟩ = ⟨𝐵, 𝐶⟩)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570   ∈ wcel 2146  Vcvv 3457  ∅c0 4286  ifcif 4489  {csn 4591  {cpr 4593  ⟨cop 4597

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 2148  ax-9 2156  ax-ext 2737

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 2744  df-cleq 2757  df-clel 2840  df-rab 3419  df-v 3459  df-dif 3909  df-un 3911  df-ss 3923  df-nul 4287  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598

This theorem is used by:  opeq12  4842  opeq1i  4843  opeq1d  4846  oteq1  4849  breq1  5114  cbvopab1  5187  cbvopab1g  5188  cbvopab1s  5190  cbvopab1v  5191  opthg  5461  eqvinop  5471  sbcop1  5472  opelopabsb  5516  opelxp  5699  elvvv  5739  opabid2  5817  opeliunxp2  5826  elsnres  6022  dmsnopg  6216  reuop  6298  funopg  6574  f1osng  6867  f1oprswap  6870  dmfco  6981  fvelrn  7075  fsng  7137  funsneqopb  7153  fprg  7156  fvrnressn  7162  funfvima3  7238  oveq1  7423  oprabidw  7447  oprabid  7448  dfoprab2  7474  cbvoprab1  7503  elxp4  7921  elxp5  7922  opabex3d  7964  opabex3rd  7965  opabex3  7966  op1stg  8000  op2ndg  8001  el2xptp  8034  dfoprab4f  8055  frxp  8124  frxp2  8142  xpord2pred  8143  opeliunxp2f  8208  tfrlem11  8377  omeu  8572  oeeui  8590  elixpsn  8937  fundmen  9031  xpsnen  9052  xpassen  9062  xpf1o  9130  unxpdomlem1  9219  djur  9917  dfac5lem1  10119  dfac5lem4  10122  axdc4lem  10450  nqereu  10925  mulcanenq  10956  archnq  10976  prlem934  11029  supsrlem  11107  supsr  11108  swrdccatin1  14780  swrdccat3blem  14794  fsum2dlem  15840  fprod2dlem  16053  vdwlem10  17068  imasaddfnlem  17600  catideu  17749  iscatd2  17755  catlid  17757  catpropd  17783  symg2bas  19487  efgmval  19806  efgi  19813  vrgpval  19861  gsumcom2  20069  rngqiprngimfo  21471  pzriprnglem10  21670  pzriprnglem11  21671  txkgen  23840  cnmpt21  23859  xkoinjcn  23875  txconn  23877  pt1hmeo  23994  cnextfvval  24253  qustgplem  24309  dvbsss  26092  axlowdim2  29341  axlowdim  29342  axcontlem10  29354  axcontlem12  29356  isnvlem  31009  br8d  33000  2ndresdju  33041  gsumhashmul  33427  gsumwrd2dccatlem  33437  rlocf1  33634  idomsubr  33670  prsrn  34345  esum2dlem  34522  eulerpartlemgvv  34807  fineqvrep  35560  satf0op  35882  satffunlem1lem1  35907  satffunlem2lem1  35909  sategoelfvb  35924  br8  36261  br6  36262  br4  36263  eldm3  36266  dfdm5  36278  elfuns  36418  brimg  36440  brapply  36441  lemsuccf  36444  brrestrict  36454  dfrdg4  36456  cgrdegen  36509  brofs  36510  cgrextend  36513  brifs  36548  ifscgr  36549  brcgr3  36551  brcolinear2  36563  colineardim1  36566  brfs  36584  idinside  36589  btwnconn1lem7  36598  btwnconn1lem11  36602  btwnconn1lem12  36603  brsegle  36613  outsideofeu  36636  fvray  36646  linedegen  36648  fvline  36649  cbvoprab1vw  36782  cbvoprab13vw  36786  cbvopab1davw  36809  cbvoprab1davw  36816  bj-inftyexpiinv  37885  bj-inftyexpidisj  37887  finxpeq2  38066  finxpreclem6  38075  finxpsuclem  38076  curfv  38284  isdivrngo  38634  drngoi  38635  dicelval3  41987  dihjatcclem4  42228  dropab1  45189  relopabVD  45642  funressndmafv2rn  47993  dfatdmfcoafv2  48024  ichnreuop  48254  ichreuopeq  48255  reuopreuprim  48308  gpgedgvtx0  48859  gpgedgvtx1  48860  gpgcubic  48877  gpg5nbgr3star  48879  pgnbgreunbgrlem3  48916  pgnbgreunbgrlem6  48922  pgnbgreunbgr  48923  sectpropdlem  49847  ssccatid  49883  upfval2  49988  isthincd2lem2  50246