Theorem opeq1 4839

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 2857	. . . 4 ⊢ (𝐴 = 𝐵 → (𝐴 ∈ V ↔ 𝐵 ∈ V))
2	1	anbi1d 642	. . 3 ⊢ (𝐴 = 𝐵 → ((𝐴 ∈ V ∧ 𝐶 ∈ V) ↔ (𝐵 ∈ V ∧ 𝐶 ∈ V)))
3		sneq 4601	. . . 4 ⊢ (𝐴 = 𝐵 → {𝐴} = {𝐵})
4		preq1 4701	. . . 4 ⊢ (𝐴 = 𝐵 → {𝐴, 𝐶} = {𝐵, 𝐶})
5	3, 4	preq12d 4709	. . 3 ⊢ (𝐴 = 𝐵 → {{𝐴}, {𝐴, 𝐶}} = {{𝐵}, {𝐵, 𝐶}})
6	2, 5	ifbieq1d 4514	. 2 ⊢ (𝐴 = 𝐵 → if((𝐴 ∈ V ∧ 𝐶 ∈ V), {{𝐴}, {𝐴, 𝐶}}, ∅) = if((𝐵 ∈ V ∧ 𝐶 ∈ V), {{𝐵}, {𝐵, 𝐶}}, ∅))
7		dfopif 4836	. 2 ⊢ ⟨𝐴, 𝐶⟩ = if((𝐴 ∈ V ∧ 𝐶 ∈ V), {{𝐴}, {𝐴, 𝐶}}, ∅)
8		dfopif 4836	. 2 ⊢ ⟨𝐵, 𝐶⟩ = if((𝐵 ∈ V ∧ 𝐶 ∈ V), {{𝐵}, {𝐵, 𝐶}}, ∅)
9	6, 7, 8	3eqtr4g 2829	1 ⊢ (𝐴 = 𝐵 → ⟨𝐴, 𝐶⟩ = ⟨𝐵, 𝐶⟩)

Syntax hints:   → wi 4   ∧ wa 400   = wceq 1567   ∈ wcel 2149  Vcvv 3463  ∅c0 4294  ifcif 4489  {csn 4591  {cpr 4593  ⟨cop 4597

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-rab 3424  df-v 3465  df-dif 3916  df-un 3918  df-ss 3930  df-nul 4295  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598

This theorem is referenced by:  opeq12  4841  opeq1i  4842  opeq1d  4845  oteq1  4848  breq1  5113  cbvopab1  5186  cbvopab1g  5187  cbvopab1s  5189  cbvopab1v  5190  opthg  5457  eqvinop  5467  sbcop1  5468  opelopabsb  5512  opelxp  5695  elvvv  5735  opabid2  5813  opeliunxp2  5822  elsnres  6018  dmsnopg  6211  reuop  6291  funopg  6567  f1osng  6861  f1oprswap  6864  dmfco  6975  fvelrn  7069  fsng  7131  funsneqopb  7147  fprg  7150  fvrnressn  7156  funfvima3  7232  oveq1  7415  oprabidw  7439  oprabid  7440  dfoprab2  7466  cbvoprab1  7495  elxp4  7915  elxp5  7916  opabex3d  7958  opabex3rd  7959  opabex3  7960  op1stg  7994  op2ndg  7995  el2xptp  8028  dfoprab4f  8049  frxp  8118  frxp2  8136  xpord2pred  8137  opeliunxp2f  8202  tfrlem11  8371  omeu  8566  oeeui  8584  elixpsn  8931  fundmen  9024  xpsnen  9045  xpassen  9055  xpf1o  9123  unxpdomlem1  9212  djur  9901  dfac5lem1  10103  dfac5lem4  10106  axdc4lem  10435  nqereu  10910  mulcanenq  10941  archnq  10961  prlem934  11014  supsrlem  11092  supsr  11093  swrdccatin1  14758  swrdccat3blem  14772  fsum2dlem  15817  fprod2dlem  16030  vdwlem10  17046  imasaddfnlem  17578  catideu  17727  iscatd2  17733  catlid  17735  catpropd  17761  symg2bas  19459  efgmval  19778  efgi  19785  vrgpval  19833  gsumcom2  20041  rngqiprngimfo  21408  pzriprnglem10  21605  pzriprnglem11  21606  txkgen  23774  cnmpt21  23793  xkoinjcn  23809  txconn  23811  pt1hmeo  23928  cnextfvval  24187  qustgplem  24243  dvbsss  26026  axlowdim2  29247  axlowdim  29248  axcontlem10  29260  axcontlem12  29262  isnvlem  30899  br8d  32890  2ndresdju  32931  gsumhashmul  33324  gsumwrd2dccatlem  33334  rlocf1  33531  idomsubr  33569  prsrn  34246  esum2dlem  34423  eulerpartlemgvv  34707  fineqvrep  35446  satf0op  35764  satffunlem1lem1  35789  satffunlem2lem1  35791  sategoelfvb  35806  br8  36143  br6  36144  br4  36145  eldm3  36148  dfdm5  36160  elfuns  36300  brimg  36322  brapply  36323  lemsuccf  36326  brrestrict  36336  dfrdg4  36338  cgrdegen  36391  brofs  36392  cgrextend  36395  brifs  36430  ifscgr  36431  brcgr3  36433  brcolinear2  36445  colineardim1  36448  brfs  36466  idinside  36471  btwnconn1lem7  36480  btwnconn1lem11  36484  btwnconn1lem12  36485  brsegle  36495  outsideofeu  36518  fvray  36528  linedegen  36530  fvline  36531  cbvoprab1vw  36634  cbvoprab13vw  36638  cbvopab1davw  36661  cbvoprab1davw  36668  bj-inftyexpiinv  37735  bj-inftyexpidisj  37737  finxpeq2  37916  finxpreclem6  37925  finxpsuclem  37926  curfv  38134  isdivrngo  38484  drngoi  38485  dicelval3  41839  dihjatcclem4  42080  dropab1  45041  relopabVD  45494  funressndmafv2rn  47842  dfatdmfcoafv2  47873  ichnreuop  48103  ichreuopeq  48104  reuopreuprim  48157  gpgedgvtx0  48708  gpgedgvtx1  48709  gpgcubic  48726  gpg5nbgr3star  48728  pgnbgreunbgrlem3  48765  pgnbgreunbgrlem6  48771  pgnbgreunbgr  48772  sectpropdlem  49692  ssccatid  49728  upfval2  49833  isthincd2lem2  50091