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 2820	. . . 4 ⊢ (𝐴 = 𝐵 → (𝐴 ∈ V ↔ 𝐵 ∈ V))
2	1	anbi1d 629	. . 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 2796	1 ⊢ (𝐴 = 𝐵 → ⟨𝐴, 𝐶⟩ = ⟨𝐵, 𝐶⟩)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2105  Vcvv 3473  ∅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 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-sb 2067  df-clab 2709  df-cleq 2723  df-clel 2809  df-rab 3432  df-v 3475  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  5751  opabid2  5828  opeliunxp2  5838  elsnres  6021  elimasngOLD  6089  dmsnopg  6212  reuop  6292  funopg  6582  f1osng  6874  f1oprswap  6877  dmfco  6987  fvelrn  7078  fsng  7137  funsneqopb  7152  fprg  7155  fvrnressn  7161  funfvima3  7240  oveq1  7419  oprabidw  7443  oprabid  7444  dfoprab2  7470  cbvoprab1  7499  elxp4  7917  elxp5  7918  opabex3d  7956  opabex3rd  7957  opabex3  7958  op1stg  7991  op2ndg  7992  el2xptp  8025  dfoprab4f  8046  frxp  8117  frxp2  8135  xpord2pred  8136  opeliunxp2f  8201  tfrlem11  8394  omeu  8591  oeeui  8608  elixpsn  8937  fundmen  9037  xpsnen  9061  xpassen  9072  xpf1o  9145  unxpdomlem1  9256  djur  9920  dfac5lem1  10124  dfac5lem4  10127  axdc4lem  10456  nqereu  10930  mulcanenq  10961  archnq  10981  prlem934  11034  supsrlem  11112  supsr  11113  swrdccatin1  14682  swrdccat3blem  14696  fsum2dlem  15723  fprod2dlem  15931  vdwlem10  16930  imasaddfnlem  17481  catideu  17626  iscatd2  17632  catlid  17634  catpropd  17660  symg2bas  19308  efgmval  19628  efgi  19635  vrgpval  19683  gsumcom2  19891  rngqiprngimfo  21149  pzriprnglem10  21350  pzriprnglem11  21351  txkgen  23476  cnmpt21  23495  xkoinjcn  23511  txconn  23513  pt1hmeo  23630  cnextfvval  23889  qustgplem  23945  dvbsss  25751  axlowdim2  28652  axlowdim  28653  axcontlem10  28665  axcontlem12  28667  isnvlem  30297  br8d  32273  2ndresdju  32308  cnvoprabOLD  32379  gsumhashmul  32645  prsrn  33360  esum2dlem  33555  eulerpartlemgvv  33840  fineqvrep  34560  satf0op  34833  satffunlem1lem1  34858  satffunlem2lem1  34860  sategoelfvb  34875  br8  35197  br6  35198  br4  35199  eldm3  35202  dfdm5  35215  elfuns  35358  brimg  35380  brapply  35381  brsuccf  35384  brrestrict  35392  dfrdg4  35394  cgrdegen  35447  brofs  35448  cgrextend  35451  brifs  35486  ifscgr  35487  brcgr3  35489  brcolinear2  35501  colineardim1  35504  brfs  35522  idinside  35527  btwnconn1lem7  35536  btwnconn1lem11  35540  btwnconn1lem12  35541  brsegle  35551  outsideofeu  35574  fvray  35584  linedegen  35586  fvline  35587  bj-inftyexpiinv  36555  bj-inftyexpidisj  36557  finxpeq2  36734  finxpreclem6  36743  finxpsuclem  36744  curfv  36934  isdivrngo  37284  drngoi  37285  dicelval3  40517  dihjatcclem4  40758  dropab1  43671  relopabVD  44127  funressndmafv2rn  46392  dfatdmfcoafv2  46423  ichnreuop  46601  ichreuopeq  46602  reuopreuprim  46655  isthincd2lem2  47820