Theorem opeq1 4402

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 2689	. . . 4 ⊢ (𝐴 = 𝐵 → (𝐴 ∈ V ↔ 𝐵 ∈ V))
2	1	anbi1d 741	. . 3 ⊢ (𝐴 = 𝐵 → ((𝐴 ∈ V ∧ 𝐶 ∈ V) ↔ (𝐵 ∈ V ∧ 𝐶 ∈ V)))
3		sneq 4187	. . . 4 ⊢ (𝐴 = 𝐵 → {𝐴} = {𝐵})
4		preq1 4268	. . . 4 ⊢ (𝐴 = 𝐵 → {𝐴, 𝐶} = {𝐵, 𝐶})
5	3, 4	preq12d 4276	. . 3 ⊢ (𝐴 = 𝐵 → {{𝐴}, {𝐴, 𝐶}} = {{𝐵}, {𝐵, 𝐶}})
6	2, 5	ifbieq1d 4109	. 2 ⊢ (𝐴 = 𝐵 → if((𝐴 ∈ V ∧ 𝐶 ∈ V), {{𝐴}, {𝐴, 𝐶}}, ∅) = if((𝐵 ∈ V ∧ 𝐶 ∈ V), {{𝐵}, {𝐵, 𝐶}}, ∅))
7		dfopif 4399	. 2 ⊢ ⟨𝐴, 𝐶⟩ = if((𝐴 ∈ V ∧ 𝐶 ∈ V), {{𝐴}, {𝐴, 𝐶}}, ∅)
8		dfopif 4399	. 2 ⊢ ⟨𝐵, 𝐶⟩ = if((𝐵 ∈ V ∧ 𝐶 ∈ V), {{𝐵}, {𝐵, 𝐶}}, ∅)
9	6, 7, 8	3eqtr4g 2681	1 ⊢ (𝐴 = 𝐵 → ⟨𝐴, 𝐶⟩ = ⟨𝐵, 𝐶⟩)

Syntax hints:   → wi 4   ∧ wa 384   = wceq 1483   ∈ wcel 1990  Vcvv 3200  ∅c0 3915  ifcif 4086  {csn 4177  {cpr 4179  ⟨cop 4183

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-rab 2921  df-v 3202  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184

This theorem is referenced by:  opeq12  4404  opeq1i  4405  opeq1d  4408  oteq1  4411  breq1  4656  cbvopab1  4723  cbvopab1s  4725  opthg  4946  eqvinop  4955  opelopabsb  4985  opelxp  5146  elvvv  5178  opabid2  5251  opeliunxp2  5260  elsnres  5436  elimasng  5491  dmsnopg  5606  cnvsng  5621  elsnxpOLD  5678  funopg  5922  f1osng  6177  f1oprswap  6180  dmfco  6272  fvelrn  6352  fsng  6404  fprg  6422  fvrnressn  6428  fvsng  6447  funfvima3  6495  oveq1  6657  oprabid  6677  dfoprab2  6701  cbvoprab1  6727  elxp4  7110  elxp5  7111  opabex3d  7145  opabex3  7146  op1stg  7180  op2ndg  7181  el2xptp  7211  dfoprab4f  7226  frxp  7287  opeliunxp2f  7336  tfrlem11  7484  omeu  7665  oeeui  7682  elixpsn  7947  fundmen  8030  xpsnen  8044  xpassen  8054  xpf1o  8122  unxpdomlem1  8164  dfac5lem1  8946  dfac5lem4  8949  axdc4lem  9277  nqereu  9751  mulcanenq  9782  archnq  9802  prlem934  9855  supsrlem  9932  supsr  9933  swrdccatin1  13483  swrdccat3blem  13495  fsum2dlem  14501  fprod2dlem  14710  vdwlem10  15694  imasaddfnlem  16188  catideu  16336  iscatd2  16342  catlid  16344  catpropd  16369  symg2bas  17818  efgmval  18125  efgi  18132  vrgpval  18180  gsumcom2  18374  txkgen  21455  cnmpt21  21474  xkoinjcn  21490  txconn  21492  pt1hmeo  21609  cnextfvval  21869  qustgplem  21924  dvbsss  23666  axlowdim2  25840  axlowdim  25841  axcontlem10  25853  axcontlem12  25855  isnvlem  27465  br8d  29422  cnvoprab  29498  prsrn  29961  esum2dlem  30154  eulerpartlemgvv  30438  br8  31646  br6  31647  br4  31648  eldm3  31651  br1steqgOLD  31674  br2ndeqgOLD  31675  dfdm5  31676  elfuns  32022  brimg  32044  brapply  32045  brsuccf  32048  brrestrict  32056  dfrdg4  32058  cgrdegen  32111  brofs  32112  cgrextend  32115  brifs  32150  ifscgr  32151  brcgr3  32153  brcolinear2  32165  colineardim1  32168  brfs  32186  idinside  32191  btwnconn1lem7  32200  btwnconn1lem11  32204  btwnconn1lem12  32205  brsegle  32215  outsideofeu  32238  fvray  32248  linedegen  32250  fvline  32251  bj-inftyexpiinv  33095  bj-inftyexpidisj  33097  finxpeq2  33224  finxpreclem6  33233  finxpsuclem  33234  curfv  33389  isdivrngo  33749  drngoi  33750  dicelval3  36469  dihjatcclem4  36710  dropab1  38651  relopabVD  39137