Theorem opeq1 4623

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 2894	. . . 4 ⊢ (𝐴 = 𝐵 → (𝐴 ∈ V ↔ 𝐵 ∈ V))
2	1	anbi1d 623	. . 3 ⊢ (𝐴 = 𝐵 → ((𝐴 ∈ V ∧ 𝐶 ∈ V) ↔ (𝐵 ∈ V ∧ 𝐶 ∈ V)))
3		sneq 4407	. . . 4 ⊢ (𝐴 = 𝐵 → {𝐴} = {𝐵})
4		preq1 4486	. . . 4 ⊢ (𝐴 = 𝐵 → {𝐴, 𝐶} = {𝐵, 𝐶})
5	3, 4	preq12d 4494	. . 3 ⊢ (𝐴 = 𝐵 → {{𝐴}, {𝐴, 𝐶}} = {{𝐵}, {𝐵, 𝐶}})
6	2, 5	ifbieq1d 4329	. 2 ⊢ (𝐴 = 𝐵 → if((𝐴 ∈ V ∧ 𝐶 ∈ V), {{𝐴}, {𝐴, 𝐶}}, ∅) = if((𝐵 ∈ V ∧ 𝐶 ∈ V), {{𝐵}, {𝐵, 𝐶}}, ∅))
7		dfopif 4620	. 2 ⊢ ⟨𝐴, 𝐶⟩ = if((𝐴 ∈ V ∧ 𝐶 ∈ V), {{𝐴}, {𝐴, 𝐶}}, ∅)
8		dfopif 4620	. 2 ⊢ ⟨𝐵, 𝐶⟩ = if((𝐵 ∈ V ∧ 𝐶 ∈ V), {{𝐵}, {𝐵, 𝐶}}, ∅)
9	6, 7, 8	3eqtr4g 2886	1 ⊢ (𝐴 = 𝐵 → ⟨𝐴, 𝐶⟩ = ⟨𝐵, 𝐶⟩)

Syntax hints:   → wi 4   ∧ wa 386   = wceq 1656   ∈ wcel 2164  Vcvv 3414  ∅c0 4144  ifcif 4306  {csn 4397  {cpr 4399  ⟨cop 4403

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1894  ax-4 1908  ax-5 2009  ax-6 2075  ax-7 2112  ax-9 2173  ax-10 2192  ax-11 2207  ax-12 2220  ax-13 2389  ax-ext 2803

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 879  df-3an 1113  df-tru 1660  df-ex 1879  df-nf 1883  df-sb 2068  df-clab 2812  df-cleq 2818  df-clel 2821  df-nfc 2958  df-rab 3126  df-v 3416  df-dif 3801  df-un 3803  df-in 3805  df-ss 3812  df-nul 4145  df-if 4307  df-sn 4398  df-pr 4400  df-op 4404

This theorem is referenced by:  opeq12  4625  opeq1i  4626  opeq1d  4629  oteq1  4632  breq1  4876  cbvopab1  4946  cbvopab1s  4948  opthg  5166  eqvinop  5175  opelopabsb  5211  opelxp  5378  elvvv  5411  opabid2  5484  opeliunxp2  5493  elsnres  5673  elimasng  5732  dmsnopg  5847  funopg  6157  f1osng  6418  f1oprswap  6421  dmfco  6519  fvelrn  6601  fsng  6654  funsneqopb  6670  fprg  6673  fvrnressn  6679  fvsngOLD  6701  funfvima3  6751  oveq1  6912  oprabid  6936  dfoprab2  6961  cbvoprab1  6987  elxp4  7372  elxp5  7373  opabex3d  7406  opabex3  7407  op1stg  7440  op2ndg  7441  el2xptp  7473  dfoprab4f  7488  frxp  7551  opeliunxp2f  7601  tfrlem11  7750  omeu  7932  oeeui  7949  elixpsn  8214  fundmen  8296  xpsnen  8313  xpassen  8323  xpf1o  8391  unxpdomlem1  8433  djur  9058  dfac5lem1  9259  dfac5lem4  9262  axdc4lem  9592  nqereu  10066  mulcanenq  10097  archnq  10117  prlem934  10170  supsrlem  10248  supsr  10249  swrdccatin1  13821  swrdccat3blem  13841  fsum2dlem  14876  fprod2dlem  15083  vdwlem10  16065  imasaddfnlem  16541  catideu  16688  iscatd2  16694  catlid  16696  catpropd  16721  symg2bas  18168  efgmval  18476  efgi  18483  vrgpval  18533  gsumcom2  18727  txkgen  21826  cnmpt21  21845  xkoinjcn  21861  txconn  21863  pt1hmeo  21980  cnextfvval  22239  qustgplem  22294  dvbsss  24065  axlowdim2  26259  axlowdim  26260  axcontlem10  26272  axcontlem12  26274  isnvlem  28009  br8d  29958  cnvoprabOLD  30035  prsrn  30495  esum2dlem  30688  eulerpartlemgvv  30972  br8  32177  br6  32178  br4  32179  eldm3  32182  dfdm5  32203  elfuns  32550  brimg  32572  brapply  32573  brsuccf  32576  brrestrict  32584  dfrdg4  32586  cgrdegen  32639  brofs  32640  cgrextend  32643  brifs  32678  ifscgr  32679  brcgr3  32681  brcolinear2  32693  colineardim1  32696  brfs  32714  idinside  32719  btwnconn1lem7  32728  btwnconn1lem11  32732  btwnconn1lem12  32733  brsegle  32743  outsideofeu  32766  fvray  32776  linedegen  32778  fvline  32779  bj-inftyexpiinv  33628  bj-inftyexpidisj  33630  finxpeq2  33762  finxpreclem6  33771  finxpsuclem  33772  curfv  33925  isdivrngo  34284  drngoi  34285  dicelval3  37248  dihjatcclem4  37489  dropab1  39482  relopabVD  39948  funressndmafv2rn  42118  dfatdmfcoafv2  42149