Theorem opeq2 4765

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
opeq2	⊢ (𝐴 = 𝐵 → ⟨𝐶, 𝐴⟩ = ⟨𝐶, 𝐵⟩)

Proof of Theorem opeq2

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		eleq1 2877	. . . 4 ⊢ (𝐴 = 𝐵 → (𝐴 ∈ V ↔ 𝐵 ∈ V))
2		preq2 4630	. . . . . 6 ⊢ (𝐴 = 𝐵 → {𝐶, 𝐴} = {𝐶, 𝐵})
3	2	preq2d 4636	. . . . 5 ⊢ (𝐴 = 𝐵 → {{𝐶}, {𝐶, 𝐴}} = {{𝐶}, {𝐶, 𝐵}})
4	3	eleq2d 2875	. . . 4 ⊢ (𝐴 = 𝐵 → (𝑥 ∈ {{𝐶}, {𝐶, 𝐴}} ↔ 𝑥 ∈ {{𝐶}, {𝐶, 𝐵}}))
5	1, 4	3anbi23d 1436	. . 3 ⊢ (𝐴 = 𝐵 → ((𝐶 ∈ V ∧ 𝐴 ∈ V ∧ 𝑥 ∈ {{𝐶}, {𝐶, 𝐴}}) ↔ (𝐶 ∈ V ∧ 𝐵 ∈ V ∧ 𝑥 ∈ {{𝐶}, {𝐶, 𝐵}})))
6	5	abbidv 2862	. 2 ⊢ (𝐴 = 𝐵 → {𝑥 ∣ (𝐶 ∈ V ∧ 𝐴 ∈ V ∧ 𝑥 ∈ {{𝐶}, {𝐶, 𝐴}})} = {𝑥 ∣ (𝐶 ∈ V ∧ 𝐵 ∈ V ∧ 𝑥 ∈ {{𝐶}, {𝐶, 𝐵}})})
7		df-op 4532	. 2 ⊢ ⟨𝐶, 𝐴⟩ = {𝑥 ∣ (𝐶 ∈ V ∧ 𝐴 ∈ V ∧ 𝑥 ∈ {{𝐶}, {𝐶, 𝐴}})}
8		df-op 4532	. 2 ⊢ ⟨𝐶, 𝐵⟩ = {𝑥 ∣ (𝐶 ∈ V ∧ 𝐵 ∈ V ∧ 𝑥 ∈ {{𝐶}, {𝐶, 𝐵}})}
9	6, 7, 8	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  opeq2i  4769  opeq2d  4772  oteq2  4775  oteq3  4776  breq2  5034  cbvopab2  5105  cbvopab2v  5108  opthg  5334  eqvinop  5343  opelopabsb  5382  dfid3  5427  opelxp  5555  relopabi  5658  opabid2  5664  elrn2g  5725  opeldmd  5739  opeldm  5740  elrn2  5785  iss  5870  elidinxp  5878  elimasng  5922  dmsnopg  6037  reuop  6112  funopg  6358  f1osng  6630  f1oprswap  6633  tz6.12f  6669  fvn0ssdmfun  6819  fsn  6874  fsng  6876  fprg  6894  fprb  6933  oveq2  7143  cbvoprab2  7221  ovg  7293  elxp4  7609  elxp5  7610  opabex3d  7648  opabex3rd  7649  opabex3  7650  op1stg  7683  op2ndg  7684  op1steq  7715  dfoprab4f  7736  fsplit  7795  seqomlem2  8070  omeu  8194  oeeui  8211  ralxpmap  8443  elixpsn  8484  ixpsnf1o  8485  mapsnend  8571  xpsnen  8584  xpassen  8594  xpf1o  8663  unxpdomlem1  8706  djulcl  9323  djurcl  9324  djur  9332  djuss  9333  djuun  9339  1stinl  9340  2ndinl  9341  1stinr  9342  2ndinr  9343  axdc4lem  9866  nqereu  10340  mulcanenq  10371  elreal  10542  ax1rid  10572  fseq1p1m1  12976  pfxval  14026  swrdccatin1  14078  swrdccat3blem  14092  wrdlen2  14297  ruclem1  15576  imasaddfnlem  16793  imasvscafn  16802  catidex  16937  catpropd  16971  funcsetcestrclem1  17396  symg2bas  18513  efgi  18837  gsumcom2  19088  mat1rhmval  21084  mat1ric  21092  txkgen  22257  cnmpt21  22276  xkoinjcn  22292  txconn  22294  xpstopnlem1  22414  qustgplem  22726  metustid  23161  axlowdim2  26754  axlowdim  26755  axcontlem2  26759  axcontlem3  26760  axcontlem4  26761  axcontlem9  26766  axcontlem10  26767  axcontlem11  26768  cusgrexg  27234  rgrusgrprc  27379  2clwwlk2clwwlk  28135  isnvlem  28393  br8d  30374  gsumhashmul  30741  prsdm  31267  eulerpartlemgvv  31744  reprsuc  31996  bnj941  32154  bnj944  32320  cvmlift2lem1  32662  cvmlift2lem12  32674  goel  32707  gonafv  32710  satf0op  32737  sat1el2xp  32739  fmla0xp  32743  sategoelfvb  32779  br8  33105  br6  33106  br4  33107  dfrn5  33130  elima4  33132  pprodss4v  33458  brimg  33511  brapply  33512  brsuccf  33515  brrestrict  33523  dfrdg4  33525  cgrtriv  33576  brofs  33579  segconeu  33585  btwntriv2  33586  transportprops  33608  brifs  33617  ifscgr  33618  brcgr3  33620  cgrxfr  33629  brcolinear2  33632  colineardim1  33635  brfs  33653  idinside  33658  btwnconn1lem7  33667  btwnconn1lem11  33671  btwnconn1lem12  33672  btwnconn1lem14  33674  brsegle  33682  seglerflx  33686  seglemin  33687  segleantisym  33689  btwnsegle  33691  outsideofeu  33705  outsidele  33706  linedegen  33717  fvline  33718  finxpreclem6  34813  finxpsuclem  34814  curfv  35037  poimirlem4  35061  poimirlem26  35083  isdivrngo  35388  drngoi  35389  iss2  35761  dibelval3  38443  diblsmopel  38467  dihjatcclem4  38717  frlmsnic  39453  dfhe3  40476  dffrege115  40679  dropab2  41152  relopabVD  41607  projf1o  41825  sge0xp  43068  hoidmv1le  43233  ichnreuop  43989  ichreuopeq  43990  reuopreuprim  44043  0aryfvalel  45048  1arymaptf1  45056  2arymaptf1  45067  prelrrx2b  45128  rrx2xpref1o  45132  rrx2plordisom  45137