Theorem opeq1 4873

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 2822	. . . 4 ⊢ (𝐴 = 𝐵 → (𝐴 ∈ V ↔ 𝐵 ∈ V))
2	1	anbi1d 631	. . 3 ⊢ (𝐴 = 𝐵 → ((𝐴 ∈ V ∧ 𝐶 ∈ V) ↔ (𝐵 ∈ V ∧ 𝐶 ∈ V)))
3		sneq 4638	. . . 4 ⊢ (𝐴 = 𝐵 → {𝐴} = {𝐵})
4		preq1 4737	. . . 4 ⊢ (𝐴 = 𝐵 → {𝐴, 𝐶} = {𝐵, 𝐶})
5	3, 4	preq12d 4745	. . 3 ⊢ (𝐴 = 𝐵 → {{𝐴}, {𝐴, 𝐶}} = {{𝐵}, {𝐵, 𝐶}})
6	2, 5	ifbieq1d 4552	. 2 ⊢ (𝐴 = 𝐵 → if((𝐴 ∈ V ∧ 𝐶 ∈ V), {{𝐴}, {𝐴, 𝐶}}, ∅) = if((𝐵 ∈ V ∧ 𝐶 ∈ V), {{𝐵}, {𝐵, 𝐶}}, ∅))
7		dfopif 4870	. 2 ⊢ ⟨𝐴, 𝐶⟩ = if((𝐴 ∈ V ∧ 𝐶 ∈ V), {{𝐴}, {𝐴, 𝐶}}, ∅)
8		dfopif 4870	. 2 ⊢ ⟨𝐵, 𝐶⟩ = if((𝐵 ∈ V ∧ 𝐶 ∈ V), {{𝐵}, {𝐵, 𝐶}}, ∅)
9	6, 7, 8	3eqtr4g 2798	1 ⊢ (𝐴 = 𝐵 → ⟨𝐴, 𝐶⟩ = ⟨𝐵, 𝐶⟩)

Syntax hints:   → wi 4   ∧ wa 397   = wceq 1542   ∈ wcel 2107  Vcvv 3475  ∅c0 4322  ifcif 4528  {csn 4628  {cpr 4630  ⟨cop 4634

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3434  df-v 3477  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635

This theorem is referenced by:  opeq12  4875  opeq1i  4876  opeq1d  4879  oteq1  4882  breq1  5151  cbvopab1  5223  cbvopab1g  5224  cbvopab1s  5226  cbvopab1v  5227  opthg  5477  eqvinop  5487  sbcop1  5488  opelopabsb  5530  opelxp  5712  elvvv  5750  opabid2  5827  opeliunxp2  5837  elsnres  6020  elimasngOLD  6087  dmsnopg  6210  reuop  6290  funopg  6580  f1osng  6872  f1oprswap  6875  dmfco  6985  fvelrn  7076  fsng  7132  funsneqopb  7147  fprg  7150  fvrnressn  7156  funfvima3  7235  oveq1  7413  oprabidw  7437  oprabid  7438  dfoprab2  7464  cbvoprab1  7493  elxp4  7910  elxp5  7911  opabex3d  7949  opabex3rd  7950  opabex3  7951  op1stg  7984  op2ndg  7985  el2xptp  8018  dfoprab4f  8039  frxp  8109  frxp2  8127  xpord2pred  8128  opeliunxp2f  8192  tfrlem11  8385  omeu  8582  oeeui  8599  elixpsn  8928  fundmen  9028  xpsnen  9052  xpassen  9063  xpf1o  9136  unxpdomlem1  9247  djur  9911  dfac5lem1  10115  dfac5lem4  10118  axdc4lem  10447  nqereu  10921  mulcanenq  10952  archnq  10972  prlem934  11025  supsrlem  11103  supsr  11104  swrdccatin1  14672  swrdccat3blem  14686  fsum2dlem  15713  fprod2dlem  15921  vdwlem10  16920  imasaddfnlem  17471  catideu  17616  iscatd2  17622  catlid  17624  catpropd  17650  symg2bas  19255  efgmval  19575  efgi  19582  vrgpval  19630  gsumcom2  19838  txkgen  23148  cnmpt21  23167  xkoinjcn  23183  txconn  23185  pt1hmeo  23302  cnextfvval  23561  qustgplem  23617  dvbsss  25411  axlowdim2  28208  axlowdim  28209  axcontlem10  28221  axcontlem12  28223  isnvlem  29851  br8d  31827  2ndresdju  31862  cnvoprabOLD  31933  gsumhashmul  32196  prsrn  32884  esum2dlem  33079  eulerpartlemgvv  33364  fineqvrep  34084  satf0op  34357  satffunlem1lem1  34382  satffunlem2lem1  34384  sategoelfvb  34399  br8  34715  br6  34716  br4  34717  eldm3  34720  dfdm5  34733  elfuns  34876  brimg  34898  brapply  34899  brsuccf  34902  brrestrict  34910  dfrdg4  34912  cgrdegen  34965  brofs  34966  cgrextend  34969  brifs  35004  ifscgr  35005  brcgr3  35007  brcolinear2  35019  colineardim1  35022  brfs  35040  idinside  35045  btwnconn1lem7  35054  btwnconn1lem11  35058  btwnconn1lem12  35059  brsegle  35069  outsideofeu  35092  fvray  35102  linedegen  35104  fvline  35105  bj-inftyexpiinv  36078  bj-inftyexpidisj  36080  finxpeq2  36257  finxpreclem6  36266  finxpsuclem  36267  curfv  36457  isdivrngo  36807  drngoi  36808  dicelval3  40040  dihjatcclem4  40281  dropab1  43192  relopabVD  43648  funressndmafv2rn  45918  dfatdmfcoafv2  45949  ichnreuop  46127  ichreuopeq  46128  reuopreuprim  46181  rngqiprngimfo  46767  isthincd2lem2  47610