Theorem opeq1 4828

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 2849	. . . 4 ⊢ (𝐴 = 𝐵 → (𝐴 ∈ V ↔ 𝐵 ∈ V))
2	1	anbi1d 640	. . 3 ⊢ (𝐴 = 𝐵 → ((𝐴 ∈ V ∧ 𝐶 ∈ V) ↔ (𝐵 ∈ V ∧ 𝐶 ∈ V)))
3		sneq 4589	. . . 4 ⊢ (𝐴 = 𝐵 → {𝐴} = {𝐵})
4		preq1 4689	. . . 4 ⊢ (𝐴 = 𝐵 → {𝐴, 𝐶} = {𝐵, 𝐶})
5	3, 4	preq12d 4697	. . 3 ⊢ (𝐴 = 𝐵 → {{𝐴}, {𝐴, 𝐶}} = {{𝐵}, {𝐵, 𝐶}})
6	2, 5	ifbieq1d 4502	. 2 ⊢ (𝐴 = 𝐵 → if((𝐴 ∈ V ∧ 𝐶 ∈ V), {{𝐴}, {𝐴, 𝐶}}, ∅) = if((𝐵 ∈ V ∧ 𝐶 ∈ V), {{𝐵}, {𝐵, 𝐶}}, ∅))
7		dfopif 4825	. 2 ⊢ ⟨𝐴, 𝐶⟩ = if((𝐴 ∈ V ∧ 𝐶 ∈ V), {{𝐴}, {𝐴, 𝐶}}, ∅)
8		dfopif 4825	. 2 ⊢ ⟨𝐵, 𝐶⟩ = if((𝐵 ∈ V ∧ 𝐶 ∈ V), {{𝐵}, {𝐵, 𝐶}}, ∅)
9	6, 7, 8	3eqtr4g 2821	1 ⊢ (𝐴 = 𝐵 → ⟨𝐴, 𝐶⟩ = ⟨𝐵, 𝐶⟩)

Syntax hints:   → wi 4   ∧ wa 399   = wceq 1559   ∈ wcel 2141  Vcvv 3453  ∅c0 4283  ifcif 4477  {csn 4579  {cpr 4581  ⟨cop 4585

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3455  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4284  df-if 4478  df-sn 4580  df-pr 4582  df-op 4586

This theorem is referenced by:  opeq12  4830  opeq1i  4831  opeq1d  4834  oteq1  4837  breq1  5100  cbvopab1  5171  cbvopab1g  5172  cbvopab1s  5174  cbvopab1v  5175  opthg  5442  eqvinop  5452  sbcop1  5453  opelopabsb  5497  opelxp  5679  elvvv  5719  opabid2  5797  opeliunxp2  5806  elsnres  6003  dmsnopg  6195  reuop  6275  funopg  6550  f1osng  6844  f1oprswap  6847  dmfco  6958  fvelrn  7052  fsng  7114  funsneqopb  7130  fprg  7133  fvrnressn  7139  funfvima3  7215  oveq1  7398  oprabidw  7422  oprabid  7423  dfoprab2  7449  cbvoprab1  7478  elxp4  7898  elxp5  7899  opabex3d  7941  opabex3rd  7942  opabex3  7943  op1stg  7977  op2ndg  7978  el2xptp  8011  dfoprab4f  8032  frxp  8100  frxp2  8118  xpord2pred  8119  opeliunxp2f  8184  tfrlem11  8353  omeu  8548  oeeui  8566  elixpsn  8913  fundmen  9006  xpsnen  9027  xpassen  9037  xpf1o  9105  unxpdomlem1  9194  djur  9871  dfac5lem1  10073  dfac5lem4  10076  dfac5lem4OLD  10078  axdc4lem  10406  nqereu  10881  mulcanenq  10912  archnq  10932  prlem934  10985  supsrlem  11063  supsr  11064  swrdccatin1  14732  swrdccat3blem  14746  fsum2dlem  15788  fprod2dlem  16001  vdwlem10  17017  imasaddfnlem  17549  catideu  17698  iscatd2  17704  catlid  17706  catpropd  17732  symg2bas  19424  efgmval  19743  efgi  19750  vrgpval  19798  gsumcom2  20006  rngqiprngimfo  21359  pzriprnglem10  21530  pzriprnglem11  21531  txkgen  23700  cnmpt21  23719  xkoinjcn  23735  txconn  23737  pt1hmeo  23854  cnextfvval  24113  qustgplem  24169  dvbsss  25952  axlowdim2  29118  axlowdim  29119  axcontlem10  29131  axcontlem12  29133  isnvlem  30770  br8d  32771  2ndresdju  32812  gsumhashmul  33208  gsumwrd2dccatlem  33218  rlocf1  33416  idomsubr  33457  prsrn  34173  esum2dlem  34350  eulerpartlemgvv  34634  fineqvrep  35371  satf0op  35688  satffunlem1lem1  35713  satffunlem2lem1  35715  sategoelfvb  35730  br8  36067  br6  36068  br4  36069  eldm3  36072  dfdm5  36084  elfuns  36224  brimg  36246  brapply  36247  lemsuccf  36250  brrestrict  36260  dfrdg4  36262  cgrdegen  36315  brofs  36316  cgrextend  36319  brifs  36354  ifscgr  36355  brcgr3  36357  brcolinear2  36369  colineardim1  36372  brfs  36390  idinside  36395  btwnconn1lem7  36404  btwnconn1lem11  36408  btwnconn1lem12  36409  brsegle  36419  outsideofeu  36442  fvray  36452  linedegen  36454  fvline  36455  cbvoprab1vw  36558  cbvoprab13vw  36562  cbvopab1davw  36585  cbvoprab1davw  36592  bj-inftyexpiinv  37661  bj-inftyexpidisj  37663  finxpeq2  37842  finxpreclem6  37851  finxpsuclem  37852  curfv  38060  isdivrngo  38410  drngoi  38411  dicelval3  41765  dihjatcclem4  42006  dropab1  44983  relopabVD  45437  funressndmafv2rn  47778  dfatdmfcoafv2  47809  ichnreuop  48039  ichreuopeq  48040  reuopreuprim  48093  gpgedgvtx0  48644  gpgedgvtx1  48645  gpgcubic  48662  gpg5nbgr3star  48664  pgnbgreunbgrlem3  48701  pgnbgreunbgrlem6  48707  pgnbgreunbgr  48708  sectpropdlem  49618  ssccatid  49654  upfval2  49759  isthincd2lem2  50017