Theorem opeq1 4878

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 631	. . 3 ⊢ (𝐴 = 𝐵 → ((𝐴 ∈ V ∧ 𝐶 ∈ V) ↔ (𝐵 ∈ V ∧ 𝐶 ∈ V)))
3		sneq 4641	. . . 4 ⊢ (𝐴 = 𝐵 → {𝐴} = {𝐵})
4		preq1 4738	. . . 4 ⊢ (𝐴 = 𝐵 → {𝐴, 𝐶} = {𝐵, 𝐶})
5	3, 4	preq12d 4746	. . 3 ⊢ (𝐴 = 𝐵 → {{𝐴}, {𝐴, 𝐶}} = {{𝐵}, {𝐵, 𝐶}})
6	2, 5	ifbieq1d 4555	. 2 ⊢ (𝐴 = 𝐵 → if((𝐴 ∈ V ∧ 𝐶 ∈ V), {{𝐴}, {𝐴, 𝐶}}, ∅) = if((𝐵 ∈ V ∧ 𝐶 ∈ V), {{𝐵}, {𝐵, 𝐶}}, ∅))
7		dfopif 4875	. 2 ⊢ ⟨𝐴, 𝐶⟩ = if((𝐴 ∈ V ∧ 𝐶 ∈ V), {{𝐴}, {𝐴, 𝐶}}, ∅)
8		dfopif 4875	. 2 ⊢ ⟨𝐵, 𝐶⟩ = if((𝐵 ∈ V ∧ 𝐶 ∈ V), {{𝐵}, {𝐵, 𝐶}}, ∅)
9	6, 7, 8	3eqtr4g 2800	1 ⊢ (𝐴 = 𝐵 → ⟨𝐴, 𝐶⟩ = ⟨𝐵, 𝐶⟩)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1537   ∈ wcel 2106  Vcvv 3478  ∅c0 4339  ifcif 4531  {csn 4631  {cpr 4633  ⟨cop 4637

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-rab 3434  df-v 3480  df-dif 3966  df-un 3968  df-ss 3980  df-nul 4340  df-if 4532  df-sn 4632  df-pr 4634  df-op 4638

This theorem is referenced by:  opeq12  4880  opeq1i  4881  opeq1d  4884  oteq1  4887  breq1  5151  cbvopab1  5223  cbvopab1g  5224  cbvopab1s  5226  cbvopab1v  5227  opthg  5488  eqvinop  5498  sbcop1  5499  opelopabsb  5540  opelxp  5725  elvvv  5764  opabid2  5841  opeliunxp2  5852  elsnres  6041  elimasngOLD  6111  dmsnopg  6235  reuop  6315  funopg  6602  f1osng  6890  f1oprswap  6893  dmfco  7005  fvelrn  7096  fsng  7157  funsneqopb  7172  fprg  7175  fvrnressn  7181  funfvima3  7256  oveq1  7438  oprabidw  7462  oprabid  7463  dfoprab2  7491  cbvoprab1  7520  elxp4  7945  elxp5  7946  opabex3d  7989  opabex3rd  7990  opabex3  7991  op1stg  8025  op2ndg  8026  el2xptp  8059  dfoprab4f  8080  frxp  8150  frxp2  8168  xpord2pred  8169  opeliunxp2f  8234  tfrlem11  8427  omeu  8622  oeeui  8639  elixpsn  8976  fundmen  9070  xpsnen  9094  xpassen  9105  xpf1o  9178  unxpdomlem1  9284  djur  9957  dfac5lem1  10161  dfac5lem4  10164  dfac5lem4OLD  10166  axdc4lem  10493  nqereu  10967  mulcanenq  10998  archnq  11018  prlem934  11071  supsrlem  11149  supsr  11150  swrdccatin1  14760  swrdccat3blem  14774  fsum2dlem  15803  fprod2dlem  16013  vdwlem10  17024  imasaddfnlem  17575  catideu  17720  iscatd2  17726  catlid  17728  catpropd  17754  symg2bas  19425  efgmval  19745  efgi  19752  vrgpval  19800  gsumcom2  20008  rngqiprngimfo  21329  pzriprnglem10  21519  pzriprnglem11  21520  txkgen  23676  cnmpt21  23695  xkoinjcn  23711  txconn  23713  pt1hmeo  23830  cnextfvval  24089  qustgplem  24145  dvbsss  25952  axlowdim2  28990  axlowdim  28991  axcontlem10  29003  axcontlem12  29005  isnvlem  30639  br8d  32630  2ndresdju  32666  cnvoprabOLD  32738  gsumhashmul  33047  gsumwrd2dccatlem  33052  rlocf1  33260  idomsubr  33291  prsrn  33876  esum2dlem  34073  eulerpartlemgvv  34358  fineqvrep  35088  satf0op  35362  satffunlem1lem1  35387  satffunlem2lem1  35389  sategoelfvb  35404  br8  35736  br6  35737  br4  35738  eldm3  35741  dfdm5  35754  elfuns  35897  brimg  35919  brapply  35920  brsuccf  35923  brrestrict  35931  dfrdg4  35933  cgrdegen  35986  brofs  35987  cgrextend  35990  brifs  36025  ifscgr  36026  brcgr3  36028  brcolinear2  36040  colineardim1  36043  brfs  36061  idinside  36066  btwnconn1lem7  36075  btwnconn1lem11  36079  btwnconn1lem12  36080  brsegle  36090  outsideofeu  36113  fvray  36123  linedegen  36125  fvline  36126  cbvoprab1vw  36220  cbvoprab13vw  36224  cbvopab1davw  36247  cbvoprab1davw  36254  bj-inftyexpiinv  37191  bj-inftyexpidisj  37193  finxpeq2  37370  finxpreclem6  37379  finxpsuclem  37380  curfv  37587  isdivrngo  37937  drngoi  37938  dicelval3  41163  dihjatcclem4  41404  dropab1  44443  relopabVD  44899  funressndmafv2rn  47173  dfatdmfcoafv2  47204  ichnreuop  47397  ichreuopeq  47398  reuopreuprim  47451  gpgedgvtx0  47954  gpgedgvtx1  47955  gpgcubic  47970  gpg5nbgr3star  47972  isthincd2lem2  48836