Theorem opeq1 4763

Description: Equality theorem for ordered pairs. (Contributed by NM, 25-Jun-1998.) (Revised by Mario Carneiro, 26-Apr-2015.) Avoid ax-10 2142, ax-11 2158, ax-12 2175. (Revised by Gino Giotto, 26-May-2024.)

Assertion

Ref	Expression
opeq1	⊢ (𝐴 = 𝐵 → ⟨𝐴, 𝐶⟩ = ⟨𝐵, 𝐶⟩)

Proof of Theorem opeq1

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		eleq1 2877	. . . 4 ⊢ (𝐴 = 𝐵 → (𝐴 ∈ V ↔ 𝐵 ∈ V))
2		sneq 4535	. . . . . 6 ⊢ (𝐴 = 𝐵 → {𝐴} = {𝐵})
3		preq1 4629	. . . . . 6 ⊢ (𝐴 = 𝐵 → {𝐴, 𝐶} = {𝐵, 𝐶})
4	2, 3	preq12d 4637	. . . . 5 ⊢ (𝐴 = 𝐵 → {{𝐴}, {𝐴, 𝐶}} = {{𝐵}, {𝐵, 𝐶}})
5	4	eleq2d 2875	. . . 4 ⊢ (𝐴 = 𝐵 → (𝑥 ∈ {{𝐴}, {𝐴, 𝐶}} ↔ 𝑥 ∈ {{𝐵}, {𝐵, 𝐶}}))
6	1, 5	3anbi13d 1435	. . 3 ⊢ (𝐴 = 𝐵 → ((𝐴 ∈ V ∧ 𝐶 ∈ V ∧ 𝑥 ∈ {{𝐴}, {𝐴, 𝐶}}) ↔ (𝐵 ∈ V ∧ 𝐶 ∈ V ∧ 𝑥 ∈ {{𝐵}, {𝐵, 𝐶}})))
7	6	abbidv 2862	. 2 ⊢ (𝐴 = 𝐵 → {𝑥 ∣ (𝐴 ∈ V ∧ 𝐶 ∈ V ∧ 𝑥 ∈ {{𝐴}, {𝐴, 𝐶}})} = {𝑥 ∣ (𝐵 ∈ V ∧ 𝐶 ∈ V ∧ 𝑥 ∈ {{𝐵}, {𝐵, 𝐶}})})
8		df-op 4532	. 2 ⊢ ⟨𝐴, 𝐶⟩ = {𝑥 ∣ (𝐴 ∈ V ∧ 𝐶 ∈ V ∧ 𝑥 ∈ {{𝐴}, {𝐴, 𝐶}})}
9		df-op 4532	. 2 ⊢ ⟨𝐵, 𝐶⟩ = {𝑥 ∣ (𝐵 ∈ V ∧ 𝐶 ∈ V ∧ 𝑥 ∈ {{𝐵}, {𝐵, 𝐶}})}
10	7, 8, 9	3eqtr4g 2858	1 ⊢ (𝐴 = 𝐵 → ⟨𝐴, 𝐶⟩ = ⟨𝐵, 𝐶⟩)

Syntax hints:   → wi 4   ∧ w3a 1084   = wceq 1538   ∈ wcel 2111  {cab 2776  Vcvv 3441  {csn 4525  {cpr 4527  ⟨cop 4531

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-un 3886  df-sn 4526  df-pr 4528  df-op 4532

This theorem is referenced by:  opeq12  4767  opeq1i  4768  opeq1d  4771  oteq1  4774  breq1  5033  cbvopab1  5103  cbvopab1g  5104  cbvopab1s  5106  opthg  5334  eqvinop  5343  sbcop1  5344  opelopabsb  5382  opelxp  5555  elvvv  5591  opabid2  5664  opeliunxp2  5673  elsnres  5858  elimasng  5922  dmsnopg  6037  reuop  6112  funopg  6358  f1osng  6630  f1oprswap  6633  dmfco  6734  fvelrn  6821  fsng  6876  funsneqopb  6891  fprg  6894  fvrnressn  6900  funfvima3  6976  oveq1  7142  oprabidw  7166  oprabid  7167  dfoprab2  7191  cbvoprab1  7220  elxp4  7609  elxp5  7610  opabex3d  7648  opabex3rd  7649  opabex3  7650  op1stg  7683  op2ndg  7684  el2xptp  7717  dfoprab4f  7736  frxp  7803  opeliunxp2f  7859  tfrlem11  8007  omeu  8194  oeeui  8211  elixpsn  8484  fundmen  8566  xpsnen  8584  xpassen  8594  xpf1o  8663  unxpdomlem1  8706  djur  9332  dfac5lem1  9534  dfac5lem4  9537  axdc4lem  9866  nqereu  10340  mulcanenq  10371  archnq  10391  prlem934  10444  supsrlem  10522  supsr  10523  swrdccatin1  14078  swrdccat3blem  14092  fsum2dlem  15117  fprod2dlem  15326  vdwlem10  16316  imasaddfnlem  16793  catideu  16938  iscatd2  16944  catlid  16946  catpropd  16971  symg2bas  18513  efgmval  18830  efgi  18837  vrgpval  18885  gsumcom2  19088  txkgen  22257  cnmpt21  22276  xkoinjcn  22292  txconn  22294  pt1hmeo  22411  cnextfvval  22670  qustgplem  22726  dvbsss  24505  axlowdim2  26754  axlowdim  26755  axcontlem10  26767  axcontlem12  26769  isnvlem  28393  br8d  30374  2ndresdju  30411  cnvoprabOLD  30482  gsumhashmul  30741  prsrn  31268  esum2dlem  31461  eulerpartlemgvv  31744  satf0op  32737  satffunlem1lem1  32762  satffunlem2lem1  32764  sategoelfvb  32779  br8  33105  br6  33106  br4  33107  eldm3  33110  dfdm5  33129  elfuns  33489  brimg  33511  brapply  33512  brsuccf  33515  brrestrict  33523  dfrdg4  33525  cgrdegen  33578  brofs  33579  cgrextend  33582  brifs  33617  ifscgr  33618  brcgr3  33620  brcolinear2  33632  colineardim1  33635  brfs  33653  idinside  33658  btwnconn1lem7  33667  btwnconn1lem11  33671  btwnconn1lem12  33672  brsegle  33682  outsideofeu  33705  fvray  33715  linedegen  33717  fvline  33718  bj-inftyexpiinv  34623  bj-inftyexpidisj  34625  finxpeq2  34804  finxpreclem6  34813  finxpsuclem  34814  curfv  35037  isdivrngo  35388  drngoi  35389  dicelval3  38476  dihjatcclem4  38717  dropab1  41151  relopabVD  41607  funressndmafv2rn  43779  dfatdmfcoafv2  43810  ichnreuop  43989  ichreuopeq  43990  reuopreuprim  44043