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  28651  axlowdim  28652  axcontlem10  28664  axcontlem12  28666  isnvlem  30296  br8d  32272  2ndresdju  32307  cnvoprabOLD  32378  gsumhashmul  32644  prsrn  33359  esum2dlem  33554  eulerpartlemgvv  33839  fineqvrep  34559  satf0op  34832  satffunlem1lem1  34857  satffunlem2lem1  34859  sategoelfvb  34874  br8  35196  br6  35197  br4  35198  eldm3  35201  dfdm5  35214  elfuns  35357  brimg  35379  brapply  35380  brsuccf  35383  brrestrict  35391  dfrdg4  35393  cgrdegen  35446  brofs  35447  cgrextend  35450  brifs  35485  ifscgr  35486  brcgr3  35488  brcolinear2  35500  colineardim1  35503  brfs  35521  idinside  35526  btwnconn1lem7  35535  btwnconn1lem11  35539  btwnconn1lem12  35540  brsegle  35550  outsideofeu  35573  fvray  35583  linedegen  35585  fvline  35586  bj-inftyexpiinv  36553  bj-inftyexpidisj  36555  finxpeq2  36732  finxpreclem6  36741  finxpsuclem  36742  curfv  36932  isdivrngo  37282  drngoi  37283  dicelval3  40515  dihjatcclem4  40756  dropab1  43669  relopabVD  44125  funressndmafv2rn  46390  dfatdmfcoafv2  46421  ichnreuop  46599  ichreuopeq  46600  reuopreuprim  46653  isthincd2lem2  47818