Theorem opeq1 4804

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 2827	. . . 4 ⊢ (𝐴 = 𝐵 → (𝐴 ∈ V ↔ 𝐵 ∈ V))
2	1	anbi1d 637	. . 3 ⊢ (𝐴 = 𝐵 → ((𝐴 ∈ V ∧ 𝐶 ∈ V) ↔ (𝐵 ∈ V ∧ 𝐶 ∈ V)))
3		sneq 4565	. . . 4 ⊢ (𝐴 = 𝐵 → {𝐴} = {𝐵})
4		preq1 4665	. . . 4 ⊢ (𝐴 = 𝐵 → {𝐴, 𝐶} = {𝐵, 𝐶})
5	3, 4	preq12d 4673	. . 3 ⊢ (𝐴 = 𝐵 → {{𝐴}, {𝐴, 𝐶}} = {{𝐵}, {𝐵, 𝐶}})
6	2, 5	ifbieq1d 4479	. 2 ⊢ (𝐴 = 𝐵 → if((𝐴 ∈ V ∧ 𝐶 ∈ V), {{𝐴}, {𝐴, 𝐶}}, ∅) = if((𝐵 ∈ V ∧ 𝐶 ∈ V), {{𝐵}, {𝐵, 𝐶}}, ∅))
7		dfopif 4801	. 2 ⊢ ⟨𝐴, 𝐶⟩ = if((𝐴 ∈ V ∧ 𝐶 ∈ V), {{𝐴}, {𝐴, 𝐶}}, ∅)
8		dfopif 4801	. 2 ⊢ ⟨𝐵, 𝐶⟩ = if((𝐵 ∈ V ∧ 𝐶 ∈ V), {{𝐵}, {𝐵, 𝐶}}, ∅)
9	6, 7, 8	3eqtr4g 2799	1 ⊢ (𝐴 = 𝐵 → ⟨𝐴, 𝐶⟩ = ⟨𝐵, 𝐶⟩)

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1547   ∈ wcel 2119  Vcvv 3431  ∅c0 4261  ifcif 4454  {csn 4555  {cpr 4557  ⟨cop 4561

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-rab 3392  df-v 3433  df-dif 3886  df-un 3888  df-ss 3900  df-nul 4262  df-if 4455  df-sn 4556  df-pr 4558  df-op 4562

This theorem is referenced by:  opeq12  4806  opeq1i  4807  opeq1d  4810  oteq1  4813  breq1  5075  cbvopab1  5146  cbvopab1g  5147  cbvopab1s  5149  cbvopab1v  5150  opthg  5417  eqvinop  5427  sbcop1  5428  opelopabsb  5472  opelxp  5654  elvvv  5694  opabid2  5771  opeliunxp2  5780  elsnres  5973  dmsnopg  6164  reuop  6244  funopg  6519  f1osng  6809  f1oprswap  6812  dmfco  6923  fvelrn  7017  fsng  7079  funsneqopb  7095  fprg  7098  fvrnressn  7104  funfvima3  7180  oveq1  7363  oprabidw  7387  oprabid  7388  dfoprab2  7414  cbvoprab1  7443  elxp4  7862  elxp5  7863  opabex3d  7907  opabex3rd  7908  opabex3  7909  op1stg  7943  op2ndg  7944  el2xptp  7977  dfoprab4f  7998  frxp  8066  frxp2  8084  xpord2pred  8085  opeliunxp2f  8150  tfrlem11  8317  omeu  8510  oeeui  8528  elixpsn  8875  fundmen  8968  xpsnen  8989  xpassen  8999  xpf1o  9067  unxpdomlem1  9156  djur  9834  dfac5lem1  10036  dfac5lem4  10039  dfac5lem4OLD  10041  axdc4lem  10368  nqereu  10843  mulcanenq  10874  archnq  10894  prlem934  10947  supsrlem  11025  supsr  11026  swrdccatin1  14678  swrdccat3blem  14692  fsum2dlem  15723  fprod2dlem  15936  vdwlem10  16952  imasaddfnlem  17483  catideu  17632  iscatd2  17638  catlid  17640  catpropd  17666  symg2bas  19359  efgmval  19678  efgi  19685  vrgpval  19733  gsumcom2  19941  rngqiprngimfo  21294  pzriprnglem10  21465  pzriprnglem11  21466  txkgen  23635  cnmpt21  23654  xkoinjcn  23670  txconn  23672  pt1hmeo  23789  cnextfvval  24048  qustgplem  24104  dvbsss  25887  axlowdim2  29047  axlowdim  29048  axcontlem10  29060  axcontlem12  29062  isnvlem  30699  br8d  32700  2ndresdju  32741  gsumhashmul  33148  gsumwrd2dccatlem  33158  rlocf1  33354  idomsubr  33393  prsrn  34099  esum2dlem  34276  eulerpartlemgvv  34560  fineqvrep  35295  satf0op  35605  satffunlem1lem1  35630  satffunlem2lem1  35632  sategoelfvb  35647  br8  35984  br6  35985  br4  35986  eldm3  35989  dfdm5  36001  elfuns  36141  brimg  36163  brapply  36164  lemsuccf  36167  brrestrict  36177  dfrdg4  36179  cgrdegen  36232  brofs  36233  cgrextend  36236  brifs  36271  ifscgr  36272  brcgr3  36274  brcolinear2  36286  colineardim1  36289  brfs  36307  idinside  36312  btwnconn1lem7  36321  btwnconn1lem11  36325  btwnconn1lem12  36326  brsegle  36336  outsideofeu  36359  fvray  36369  linedegen  36371  fvline  36372  cbvoprab1vw  36465  cbvoprab13vw  36469  cbvopab1davw  36492  cbvoprab1davw  36499  bj-inftyexpiinv  37568  bj-inftyexpidisj  37570  finxpeq2  37749  finxpreclem6  37758  finxpsuclem  37759  curfv  37967  isdivrngo  38317  drngoi  38318  dicelval3  41672  dihjatcclem4  41913  dropab1  44890  relopabVD  45344  funressndmafv2rn  47686  dfatdmfcoafv2  47717  ichnreuop  47947  ichreuopeq  47948  reuopreuprim  48001  gpgedgvtx0  48552  gpgedgvtx1  48553  gpgcubic  48570  gpg5nbgr3star  48572  pgnbgreunbgrlem3  48609  pgnbgreunbgrlem6  48615  pgnbgreunbgr  48616  sectpropdlem  49526  ssccatid  49562  upfval2  49667  isthincd2lem2  49925