Theorem opeq1 4833

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 4595	. . . 4 ⊢ (𝐴 = 𝐵 → {𝐴} = {𝐵})
4		preq1 4693	. . . 4 ⊢ (𝐴 = 𝐵 → {𝐴, 𝐶} = {𝐵, 𝐶})
5	3, 4	preq12d 4701	. . 3 ⊢ (𝐴 = 𝐵 → {{𝐴}, {𝐴, 𝐶}} = {{𝐵}, {𝐵, 𝐶}})
6	2, 5	ifbieq1d 4509	. 2 ⊢ (𝐴 = 𝐵 → if((𝐴 ∈ V ∧ 𝐶 ∈ V), {{𝐴}, {𝐴, 𝐶}}, ∅) = if((𝐵 ∈ V ∧ 𝐶 ∈ V), {{𝐵}, {𝐵, 𝐶}}, ∅))
7		dfopif 4830	. 2 ⊢ ⟨𝐴, 𝐶⟩ = if((𝐴 ∈ V ∧ 𝐶 ∈ V), {{𝐴}, {𝐴, 𝐶}}, ∅)
8		dfopif 4830	. 2 ⊢ ⟨𝐵, 𝐶⟩ = if((𝐵 ∈ V ∧ 𝐶 ∈ V), {{𝐵}, {𝐵, 𝐶}}, ∅)
9	6, 7, 8	3eqtr4g 2789	1 ⊢ (𝐴 = 𝐵 → ⟨𝐴, 𝐶⟩ = ⟨𝐵, 𝐶⟩)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2109  Vcvv 3444  ∅c0 4292  ifcif 4484  {csn 4585  {cpr 4587  ⟨cop 4591

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 3403  df-v 3446  df-dif 3914  df-un 3916  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592

This theorem is referenced by:  opeq12  4835  opeq1i  4836  opeq1d  4839  oteq1  4842  breq1  5105  cbvopab1  5176  cbvopab1g  5177  cbvopab1s  5179  cbvopab1v  5180  opthg  5432  eqvinop  5442  sbcop1  5443  opelopabsb  5485  opelxp  5667  elvvv  5707  opabid2  5782  opeliunxp2  5792  elsnres  5981  dmsnopg  6174  reuop  6254  funopg  6534  f1osng  6823  f1oprswap  6826  dmfco  6939  fvelrn  7030  fsng  7091  funsneqopb  7106  fprg  7109  fvrnressn  7115  funfvima3  7192  oveq1  7376  oprabidw  7400  oprabid  7401  dfoprab2  7427  cbvoprab1  7456  elxp4  7878  elxp5  7879  opabex3d  7923  opabex3rd  7924  opabex3  7925  op1stg  7959  op2ndg  7960  el2xptp  7993  dfoprab4f  8014  frxp  8082  frxp2  8100  xpord2pred  8101  opeliunxp2f  8166  tfrlem11  8333  omeu  8526  oeeui  8543  elixpsn  8887  fundmen  8979  xpsnen  9002  xpassen  9012  xpf1o  9080  unxpdomlem1  9173  djur  9848  dfac5lem1  10052  dfac5lem4  10055  dfac5lem4OLD  10057  axdc4lem  10384  nqereu  10858  mulcanenq  10889  archnq  10909  prlem934  10962  supsrlem  11040  supsr  11041  swrdccatin1  14666  swrdccat3blem  14680  fsum2dlem  15712  fprod2dlem  15922  vdwlem10  16937  imasaddfnlem  17467  catideu  17612  iscatd2  17618  catlid  17620  catpropd  17646  symg2bas  19299  efgmval  19618  efgi  19625  vrgpval  19673  gsumcom2  19881  rngqiprngimfo  21187  pzriprnglem10  21376  pzriprnglem11  21377  txkgen  23515  cnmpt21  23534  xkoinjcn  23550  txconn  23552  pt1hmeo  23669  cnextfvval  23928  qustgplem  23984  dvbsss  25779  axlowdim2  28863  axlowdim  28864  axcontlem10  28876  axcontlem12  28878  isnvlem  30512  br8d  32511  2ndresdju  32546  gsumhashmul  32974  gsumwrd2dccatlem  32979  rlocf1  33197  idomsubr  33232  prsrn  33878  esum2dlem  34055  eulerpartlemgvv  34340  fineqvrep  35058  satf0op  35337  satffunlem1lem1  35362  satffunlem2lem1  35364  sategoelfvb  35379  br8  35716  br6  35717  br4  35718  eldm3  35721  dfdm5  35733  elfuns  35876  brimg  35898  brapply  35899  brsuccf  35902  brrestrict  35910  dfrdg4  35912  cgrdegen  35965  brofs  35966  cgrextend  35969  brifs  36004  ifscgr  36005  brcgr3  36007  brcolinear2  36019  colineardim1  36022  brfs  36040  idinside  36045  btwnconn1lem7  36054  btwnconn1lem11  36058  btwnconn1lem12  36059  brsegle  36069  outsideofeu  36092  fvray  36102  linedegen  36104  fvline  36105  cbvoprab1vw  36198  cbvoprab13vw  36202  cbvopab1davw  36225  cbvoprab1davw  36232  bj-inftyexpiinv  37169  bj-inftyexpidisj  37171  finxpeq2  37348  finxpreclem6  37357  finxpsuclem  37358  curfv  37567  isdivrngo  37917  drngoi  37918  dicelval3  41147  dihjatcclem4  41388  dropab1  44409  relopabVD  44863  funressndmafv2rn  47197  dfatdmfcoafv2  47228  ichnreuop  47446  ichreuopeq  47447  reuopreuprim  47500  gpgedgvtx0  48025  gpgedgvtx1  48026  gpgcubic  48043  gpg5nbgr3star  48045  pgnbgreunbgrlem3  48081  pgnbgreunbgrlem6  48087  pgnbgreunbgr  48088  sectpropdlem  48998  ssccatid  49034  upfval2  49139  isthincd2lem2  49397