Theorem opeq1 4826

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 2821	. . . 4 ⊢ (𝐴 = 𝐵 → (𝐴 ∈ V ↔ 𝐵 ∈ V))
2	1	anbi1d 631	. . 3 ⊢ (𝐴 = 𝐵 → ((𝐴 ∈ V ∧ 𝐶 ∈ V) ↔ (𝐵 ∈ V ∧ 𝐶 ∈ V)))
3		sneq 4587	. . . 4 ⊢ (𝐴 = 𝐵 → {𝐴} = {𝐵})
4		preq1 4687	. . . 4 ⊢ (𝐴 = 𝐵 → {𝐴, 𝐶} = {𝐵, 𝐶})
5	3, 4	preq12d 4695	. . 3 ⊢ (𝐴 = 𝐵 → {{𝐴}, {𝐴, 𝐶}} = {{𝐵}, {𝐵, 𝐶}})
6	2, 5	ifbieq1d 4501	. 2 ⊢ (𝐴 = 𝐵 → if((𝐴 ∈ V ∧ 𝐶 ∈ V), {{𝐴}, {𝐴, 𝐶}}, ∅) = if((𝐵 ∈ V ∧ 𝐶 ∈ V), {{𝐵}, {𝐵, 𝐶}}, ∅))
7		dfopif 4823	. 2 ⊢ ⟨𝐴, 𝐶⟩ = if((𝐴 ∈ V ∧ 𝐶 ∈ V), {{𝐴}, {𝐴, 𝐶}}, ∅)
8		dfopif 4823	. 2 ⊢ ⟨𝐵, 𝐶⟩ = if((𝐵 ∈ V ∧ 𝐶 ∈ V), {{𝐵}, {𝐵, 𝐶}}, ∅)
9	6, 7, 8	3eqtr4g 2793	1 ⊢ (𝐴 = 𝐵 → ⟨𝐴, 𝐶⟩ = ⟨𝐵, 𝐶⟩)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1541   ∈ wcel 2113  Vcvv 3437  ∅c0 4282  ifcif 4476  {csn 4577  {cpr 4579  ⟨cop 4583

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-rab 3397  df-v 3439  df-dif 3901  df-un 3903  df-ss 3915  df-nul 4283  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584

This theorem is referenced by:  opeq12  4828  opeq1i  4829  opeq1d  4832  oteq1  4835  breq1  5098  cbvopab1  5169  cbvopab1g  5170  cbvopab1s  5172  cbvopab1v  5173  opthg  5422  eqvinop  5432  sbcop1  5433  opelopabsb  5475  opelxp  5657  elvvv  5697  opabid2  5774  opeliunxp2  5784  elsnres  5977  dmsnopg  6168  reuop  6248  funopg  6523  f1osng  6813  f1oprswap  6816  dmfco  6927  fvelrn  7018  fsng  7079  funsneqopb  7094  fprg  7097  fvrnressn  7103  funfvima3  7179  oveq1  7362  oprabidw  7386  oprabid  7387  dfoprab2  7413  cbvoprab1  7442  elxp4  7861  elxp5  7862  opabex3d  7906  opabex3rd  7907  opabex3  7908  op1stg  7942  op2ndg  7943  el2xptp  7976  dfoprab4f  7997  frxp  8065  frxp2  8083  xpord2pred  8084  opeliunxp2f  8149  tfrlem11  8316  omeu  8509  oeeui  8526  elixpsn  8871  fundmen  8964  xpsnen  8985  xpassen  8995  xpf1o  9063  unxpdomlem1  9151  djur  9823  dfac5lem1  10025  dfac5lem4  10028  dfac5lem4OLD  10030  axdc4lem  10357  nqereu  10831  mulcanenq  10862  archnq  10882  prlem934  10935  supsrlem  11013  supsr  11014  swrdccatin1  14639  swrdccat3blem  14653  fsum2dlem  15684  fprod2dlem  15894  vdwlem10  16909  imasaddfnlem  17440  catideu  17589  iscatd2  17595  catlid  17597  catpropd  17623  symg2bas  19313  efgmval  19632  efgi  19639  vrgpval  19687  gsumcom2  19895  rngqiprngimfo  21247  pzriprnglem10  21436  pzriprnglem11  21437  txkgen  23587  cnmpt21  23606  xkoinjcn  23622  txconn  23624  pt1hmeo  23741  cnextfvval  24000  qustgplem  24056  dvbsss  25850  axlowdim2  28959  axlowdim  28960  axcontlem10  28972  axcontlem12  28974  isnvlem  30611  br8d  32612  2ndresdju  32653  gsumhashmul  33078  gsumwrd2dccatlem  33087  rlocf1  33283  idomsubr  33319  prsrn  34000  esum2dlem  34177  eulerpartlemgvv  34461  fineqvrep  35209  satf0op  35493  satffunlem1lem1  35518  satffunlem2lem1  35520  sategoelfvb  35535  br8  35872  br6  35873  br4  35874  eldm3  35877  dfdm5  35889  elfuns  36029  brimg  36051  brapply  36052  lemsuccf  36055  brrestrict  36065  dfrdg4  36067  cgrdegen  36120  brofs  36121  cgrextend  36124  brifs  36159  ifscgr  36160  brcgr3  36162  brcolinear2  36174  colineardim1  36177  brfs  36195  idinside  36200  btwnconn1lem7  36209  btwnconn1lem11  36213  btwnconn1lem12  36214  brsegle  36224  outsideofeu  36247  fvray  36257  linedegen  36259  fvline  36260  cbvoprab1vw  36353  cbvoprab13vw  36357  cbvopab1davw  36380  cbvoprab1davw  36387  bj-inftyexpiinv  37325  bj-inftyexpidisj  37327  finxpeq2  37504  finxpreclem6  37513  finxpsuclem  37514  curfv  37713  isdivrngo  38063  drngoi  38064  dicelval3  41352  dihjatcclem4  41593  dropab1  44603  relopabVD  45057  funressndmafv2rn  47385  dfatdmfcoafv2  47416  ichnreuop  47634  ichreuopeq  47635  reuopreuprim  47688  gpgedgvtx0  48223  gpgedgvtx1  48224  gpgcubic  48241  gpg5nbgr3star  48243  pgnbgreunbgrlem3  48280  pgnbgreunbgrlem6  48286  pgnbgreunbgr  48287  sectpropdlem  49197  ssccatid  49233  upfval2  49338  isthincd2lem2  49596