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 2848	. . . 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 2820	1 ⊢ (𝐴 = 𝐵 → ⟨𝐴, 𝐶⟩ = ⟨𝐵, 𝐶⟩)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570   ∈ wcel 2145  Vcvv 3450  ∅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 2732

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 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  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  5453  eqvinop  5463  sbcop1  5464  opelopabsb  5508  opelxp  5691  elvvv  5731  opabid2  5809  opeliunxp2  5818  elsnres  6014  dmsnopg  6209  reuop  6291  funopg  6567  f1osng  6860  f1oprswap  6863  dmfco  6974  fvelrn  7069  fsng  7131  funsneqopb  7149  fprg  7152  fvrnressn  7158  funfvima3  7235  oveq1  7420  oprabidw  7444  oprabid  7445  dfoprab2  7471  cbvoprab1  7500  elxp4  7919  elxp5  7920  opabex3d  7962  opabex3rd  7963  opabex3  7964  op1stg  7998  op2ndg  7999  el2xptp  8032  dfoprab4f  8053  frxp  8124  frxp2  8142  xpord2pred  8143  opeliunxp2f  8208  tfrlem11  8377  omeu  8572  oeeui  8590  curfv  8871  elixpsn  8944  fundmen  9038  xpsnen  9059  xpassen  9069  xpf1o  9137  unxpdomlem1  9226  djur  9924  dfac5lem1  10126  dfac5lem4  10129  axdc4lem  10457  nqereu  10938  mulcanenq  10969  archnq  10989  prlem934  11042  supsrlem  11120  supsr  11121  swrdccatin1  14794  swrdccat3blem  14808  fsum2dlem  15856  fprod2dlem  16067  vdwlem10  17082  imasaddfnlem  17614  catideu  17763  iscatd2  17769  catlid  17771  catpropd  17797  degenmgm2nfun  19052  symg2bas  19520  efgmval  19839  efgi  19846  vrgpval  19894  gsumcom2  20102  rngqiprngimfo  21504  pzriprnglem10  21703  pzriprnglem11  21704  txkgen  23878  cnmpt21  23897  xkoinjcn  23913  txconn  23915  pt1hmeo  24032  cnextfvval  24291  qustgplem  24347  dvbsss  26129  axlowdim2  29417  axlowdim  29418  axcontlem10  29430  axcontlem12  29432  isnvlem  31091  br8d  33081  2ndresdju  33122  gsumhashmul  33507  gsumwrd2dccatlem  33517  rlocf1  33714  idomsubr  33750  prsrn  34425  esum2dlem  34602  eulerpartlemgvv  34887  fineqvrep  35640  satf0op  35956  satffunlem1lem1  35981  satffunlem2lem1  35983  sategoelfvb  35998  br8  36335  br6  36336  br4  36337  eldm3  36340  dfdm5  36352  elfuns  36492  brimg  36514  brapply  36515  lemsuccf  36518  brrestrict  36528  dfrdg4  36530  cgrdegen  36584  brofs  36585  cgrextend  36588  brifs  36623  ifscgr  36624  brcgr3  36626  brcolinear2  36638  colineardim1  36641  brfs  36659  idinside  36664  btwnconn1lem7  36673  btwnconn1lem11  36677  btwnconn1lem12  36678  brsegle  36688  outsideofeu  36711  fvray  36721  linedegen  36723  fvline  36724  cbvoprab1vw  36857  cbvoprab13vw  36861  cbvopab1davw  36884  cbvoprab1davw  36891  bj-inftyexpiinv  37960  bj-inftyexpidisj  37962  finxpeq2  38141  finxpreclem6  38150  finxpsuclem  38151  isdivrngo  38700  drngoi  38701  dicelval3  42053  dihjatcclem4  42294  dropab1  45270  relopabVD  45723  funressndmafv2rn  48111  dfatdmfcoafv2  48142  ichnreuop  48372  ichreuopeq  48373  reuopreuprim  48426  gpgedgvtx0  48977  gpgedgvtx1  48978  gpgcubic  48995  gpg5nbgr3star  48997  pgnbgreunbgrlem3  49034  pgnbgreunbgrlem6  49040  pgnbgreunbgr  49041  sectpropdlem  49962  ssccatid  49998  upfval2  50103  isthincd2lem2  50361