Theorem opeq1 4833

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 2849	. . . 4 ⊢ (𝐴 = 𝐵 → (𝐴 ∈ V ↔ 𝐵 ∈ V))
2	1	anbi1d 643	. . 3 ⊢ (𝐴 = 𝐵 → ((𝐴 ∈ V ∧ 𝐶 ∈ V) ↔ (𝐵 ∈ V ∧ 𝐶 ∈ V)))
3		sneq 4594	. . . 4 ⊢ (𝐴 = 𝐵 → {𝐴} = {𝐵})
4		preq1 4694	. . . 4 ⊢ (𝐴 = 𝐵 → {𝐴, 𝐶} = {𝐵, 𝐶})
5	3, 4	preq12d 4702	. . 3 ⊢ (𝐴 = 𝐵 → {{𝐴}, {𝐴, 𝐶}} = {{𝐵}, {𝐵, 𝐶}})
6	2, 5	ifbieq1d 4507	. 2 ⊢ (𝐴 = 𝐵 → if((𝐴 ∈ V ∧ 𝐶 ∈ V), {{𝐴}, {𝐴, 𝐶}}, ∅) = if((𝐵 ∈ V ∧ 𝐶 ∈ V), {{𝐵}, {𝐵, 𝐶}}, ∅))
7		dfopif 4830	. 2 ⊢ ⟨𝐴, 𝐶⟩ = if((𝐴 ∈ V ∧ 𝐶 ∈ V), {{𝐴}, {𝐴, 𝐶}}, ∅)
8		dfopif 4830	. 2 ⊢ ⟨𝐵, 𝐶⟩ = if((𝐵 ∈ V ∧ 𝐶 ∈ V), {{𝐵}, {𝐵, 𝐶}}, ∅)
9	6, 7, 8	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  opeq1i  4836  opeq1d  4839  oteq1  4842  breq1  5106  cbvopab1  5179  cbvopab1g  5180  cbvopab1s  5182  cbvopab1v  5183  opthg  5446  eqvinop  5456  sbcop1  5458  opelopabsb  5504  opelxp  5687  elvvv  5727  opabid2  5806  opeliunxp2  5815  el2xptp  5820  elsnres  6010  dmsnopg  6213  reuop  6295  funopg  6572  f1osng  6865  f1oprswap  6868  dmfco  6979  fvelrn  7074  fsng  7136  funsneqopb  7154  fprg  7157  fvrnressn  7163  funfvima3  7240  oveq1  7425  oprabidw  7449  oprabid  7450  dfoprab2  7476  cbvoprab1  7505  elxp4  7932  elxp5  7933  opabex3d  7975  opabex3rd  7976  opabex3  7977  op1stg  8011  op2ndg  8012  dfoprab4f  8065  frxp  8136  frxp2  8154  xpord2pred  8155  opeliunxp2f  8220  tfrlem11  8389  omeu  8586  oeeui  8604  curfv  8885  elixpsn  8958  fundmen  9052  xpsnen  9073  xpassen  9083  xpf1o  9151  unxpdomlem1  9240  djur  9993  dfac5lem1  10195  dfac5lem4  10198  axdc4lem  10526  nqereu  11007  mulcanenq  11038  archnq  11058  prlem934  11111  supsrlem  11189  supsr  11190  swrdccatin1  14867  swrdccat3blem  14881  fsum2dlem  15929  fprod2dlem  16140  vdwlem10  17161  imasaddfnlem  17693  catideu  17842  iscatd2  17848  catlid  17850  catpropd  17876  degenmgm2nfun  19132  symg2bas  19600  efgmval  19919  efgi  19926  vrgpval  19974  gsumcom2  20182  rngqiprngimfo  21590  pzriprnglem10  21789  pzriprnglem11  21790  txkgen  23964  cnmpt21  23983  xkoinjcn  23999  txconn  24001  pt1hmeo  24118  cnextfvval  24377  qustgplem  24433  dvbsss  26215  axlowdim2  29531  axlowdim  29532  axcontlem10  29544  axcontlem12  29546  isnvlem  31205  br8d  33195  2ndresdju  33236  gsumhashmul  33621  gsumwrd2dccatlem  33631  rlocf1  33828  idomsubr  33864  prsrn  34540  esum2dlem  34717  eulerpartlemgvv  35001  fineqvrep  35765  satf0op  36121  satffunlem1lem1  36146  satffunlem2lem1  36148  sategoelfvb  36163  br8  36500  br6  36501  br4  36502  eldm3  36505  dfdm5  36517  elfuns  36657  brimg  36679  brapply  36680  lemsuccf  36683  brrestrict  36693  dfrdg4  36695  cgrdegen  36749  brofs  36750  cgrextend  36753  brifs  36788  ifscgr  36789  brcgr3  36791  brcolinear2  36803  colineardim1  36806  brfs  36824  idinside  36829  btwnconn1lem7  36838  btwnconn1lem11  36842  btwnconn1lem12  36843  brsegle  36853  outsideofeu  36876  fvray  36886  linedegen  36888  fvline  36889  cbvoprab1vw  37006  cbvoprab13vw  37010  cbvopab1davw  37033  cbvoprab1davw  37040  bj-inftyexpiinv  38109  bj-inftyexpidisj  38111  finxpeq2  38290  finxpreclem6  38299  finxpsuclem  38300  isdivrngo  38864  drngoi  38865  dicelval3  42217  dihjatcclem4  42458  dropab1  45415  relopabVD  45868  funressndmafv2rn  48262  dfatdmfcoafv2  48293  ichnreuop  48523  ichreuopeq  48524  reuopreuprim  48577  gpgedgvtx0  49128  gpgedgvtx1  49129  gpgcubic  49146  gpg5nbgr3star  49148  pgnbgreunbgrlem3  49185  pgnbgreunbgrlem6  49191  pgnbgreunbgr  49192  sectpropdlem  50113  ssccatid  50149  upfval2  50254  isthincd2lem2  50512