Theorem opeq1 4837

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 2816	. . . 4 ⊢ (𝐴 = 𝐵 → (𝐴 ∈ V ↔ 𝐵 ∈ V))
2	1	anbi1d 631	. . 3 ⊢ (𝐴 = 𝐵 → ((𝐴 ∈ V ∧ 𝐶 ∈ V) ↔ (𝐵 ∈ V ∧ 𝐶 ∈ V)))
3		sneq 4599	. . . 4 ⊢ (𝐴 = 𝐵 → {𝐴} = {𝐵})
4		preq1 4697	. . . 4 ⊢ (𝐴 = 𝐵 → {𝐴, 𝐶} = {𝐵, 𝐶})
5	3, 4	preq12d 4705	. . 3 ⊢ (𝐴 = 𝐵 → {{𝐴}, {𝐴, 𝐶}} = {{𝐵}, {𝐵, 𝐶}})
6	2, 5	ifbieq1d 4513	. 2 ⊢ (𝐴 = 𝐵 → if((𝐴 ∈ V ∧ 𝐶 ∈ V), {{𝐴}, {𝐴, 𝐶}}, ∅) = if((𝐵 ∈ V ∧ 𝐶 ∈ V), {{𝐵}, {𝐵, 𝐶}}, ∅))
7		dfopif 4834	. 2 ⊢ ⟨𝐴, 𝐶⟩ = if((𝐴 ∈ V ∧ 𝐶 ∈ V), {{𝐴}, {𝐴, 𝐶}}, ∅)
8		dfopif 4834	. 2 ⊢ ⟨𝐵, 𝐶⟩ = if((𝐵 ∈ V ∧ 𝐶 ∈ V), {{𝐵}, {𝐵, 𝐶}}, ∅)
9	6, 7, 8	3eqtr4g 2789	1 ⊢ (𝐴 = 𝐵 → ⟨𝐴, 𝐶⟩ = ⟨𝐵, 𝐶⟩)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2109  Vcvv 3447  ∅c0 4296  ifcif 4488  {csn 4589  {cpr 4591  ⟨cop 4595

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596

This theorem is referenced by:  opeq12  4839  opeq1i  4840  opeq1d  4843  oteq1  4846  breq1  5110  cbvopab1  5181  cbvopab1g  5182  cbvopab1s  5184  cbvopab1v  5185  opthg  5437  eqvinop  5447  sbcop1  5448  opelopabsb  5490  opelxp  5674  elvvv  5714  opabid2  5791  opeliunxp2  5802  elsnres  5992  dmsnopg  6186  reuop  6266  funopg  6550  f1osng  6841  f1oprswap  6844  dmfco  6957  fvelrn  7048  fsng  7109  funsneqopb  7124  fprg  7127  fvrnressn  7133  funfvima3  7210  oveq1  7394  oprabidw  7418  oprabid  7419  dfoprab2  7447  cbvoprab1  7476  elxp4  7898  elxp5  7899  opabex3d  7944  opabex3rd  7945  opabex3  7946  op1stg  7980  op2ndg  7981  el2xptp  8014  dfoprab4f  8035  frxp  8105  frxp2  8123  xpord2pred  8124  opeliunxp2f  8189  tfrlem11  8356  omeu  8549  oeeui  8566  elixpsn  8910  fundmen  9002  xpsnen  9025  xpassen  9035  xpf1o  9103  unxpdomlem1  9197  djur  9872  dfac5lem1  10076  dfac5lem4  10079  dfac5lem4OLD  10081  axdc4lem  10408  nqereu  10882  mulcanenq  10913  archnq  10933  prlem934  10986  supsrlem  11064  supsr  11065  swrdccatin1  14690  swrdccat3blem  14704  fsum2dlem  15736  fprod2dlem  15946  vdwlem10  16961  imasaddfnlem  17491  catideu  17636  iscatd2  17642  catlid  17644  catpropd  17670  symg2bas  19323  efgmval  19642  efgi  19649  vrgpval  19697  gsumcom2  19905  rngqiprngimfo  21211  pzriprnglem10  21400  pzriprnglem11  21401  txkgen  23539  cnmpt21  23558  xkoinjcn  23574  txconn  23576  pt1hmeo  23693  cnextfvval  23952  qustgplem  24008  dvbsss  25803  axlowdim2  28887  axlowdim  28888  axcontlem10  28900  axcontlem12  28902  isnvlem  30539  br8d  32538  2ndresdju  32573  gsumhashmul  33001  gsumwrd2dccatlem  33006  rlocf1  33224  idomsubr  33259  prsrn  33905  esum2dlem  34082  eulerpartlemgvv  34367  fineqvrep  35085  satf0op  35364  satffunlem1lem1  35389  satffunlem2lem1  35391  sategoelfvb  35406  br8  35743  br6  35744  br4  35745  eldm3  35748  dfdm5  35760  elfuns  35903  brimg  35925  brapply  35926  brsuccf  35929  brrestrict  35937  dfrdg4  35939  cgrdegen  35992  brofs  35993  cgrextend  35996  brifs  36031  ifscgr  36032  brcgr3  36034  brcolinear2  36046  colineardim1  36049  brfs  36067  idinside  36072  btwnconn1lem7  36081  btwnconn1lem11  36085  btwnconn1lem12  36086  brsegle  36096  outsideofeu  36119  fvray  36129  linedegen  36131  fvline  36132  cbvoprab1vw  36225  cbvoprab13vw  36229  cbvopab1davw  36252  cbvoprab1davw  36259  bj-inftyexpiinv  37196  bj-inftyexpidisj  37198  finxpeq2  37375  finxpreclem6  37384  finxpsuclem  37385  curfv  37594  isdivrngo  37944  drngoi  37945  dicelval3  41174  dihjatcclem4  41415  dropab1  44436  relopabVD  44890  funressndmafv2rn  47221  dfatdmfcoafv2  47252  ichnreuop  47470  ichreuopeq  47471  reuopreuprim  47524  gpgedgvtx0  48049  gpgedgvtx1  48050  gpgcubic  48067  gpg5nbgr3star  48069  pgnbgreunbgrlem3  48105  pgnbgreunbgrlem6  48111  pgnbgreunbgr  48112  sectpropdlem  49022  ssccatid  49058  upfval2  49163  isthincd2lem2  49421