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 2851	. . . 4 ⊢ (𝐴 = 𝐵 → (𝐴 ∈ V ↔ 𝐵 ∈ V))
2	1	anbi1d 642	. . 3 ⊢ (𝐴 = 𝐵 → ((𝐴 ∈ V ∧ 𝐶 ∈ V) ↔ (𝐵 ∈ V ∧ 𝐶 ∈ V)))
3		sneq 4600	. . . 4 ⊢ (𝐴 = 𝐵 → {𝐴} = {𝐵})
4		preq1 4700	. . . 4 ⊢ (𝐴 = 𝐵 → {𝐴, 𝐶} = {𝐵, 𝐶})
5	3, 4	preq12d 4708	. . 3 ⊢ (𝐴 = 𝐵 → {{𝐴}, {𝐴, 𝐶}} = {{𝐵}, {𝐵, 𝐶}})
6	2, 5	ifbieq1d 4513	. 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 2823	1 ⊢ (𝐴 = 𝐵 → ⟨𝐴, 𝐶⟩ = ⟨𝐵, 𝐶⟩)

Syntax hints:   → wi 4   ∧ wa 400   = wceq 1570   ∈ wcel 2143  Vcvv 3455  ∅c0 4287  ifcif 4488  {csn 4590  {cpr 4592  ⟨cop 4596

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3417  df-v 3457  df-dif 3909  df-un 3911  df-ss 3923  df-nul 4288  df-if 4489  df-sn 4591  df-pr 4593  df-op 4597

This theorem is referenced by:  opeq12  4841  opeq1i  4842  opeq1d  4845  oteq1  4848  breq1  5113  cbvopab1  5186  cbvopab1g  5187  cbvopab1s  5189  cbvopab1v  5190  opthg  5461  eqvinop  5471  sbcop1  5472  opelopabsb  5516  opelxp  5699  elvvv  5739  opabid2  5817  opeliunxp2  5826  elsnres  6022  dmsnopg  6216  reuop  6296  funopg  6572  f1osng  6865  f1oprswap  6868  dmfco  6979  fvelrn  7073  fsng  7135  funsneqopb  7151  fprg  7154  fvrnressn  7160  funfvima3  7236  oveq1  7419  oprabidw  7443  oprabid  7444  dfoprab2  7470  cbvoprab1  7499  elxp4  7920  elxp5  7921  opabex3d  7963  opabex3rd  7964  opabex3  7965  op1stg  7999  op2ndg  8000  el2xptp  8033  dfoprab4f  8054  frxp  8123  frxp2  8141  xpord2pred  8142  opeliunxp2f  8207  tfrlem11  8376  omeu  8571  oeeui  8589  elixpsn  8936  fundmen  9029  xpsnen  9050  xpassen  9060  xpf1o  9128  unxpdomlem1  9217  djur  9906  dfac5lem1  10108  dfac5lem4  10111  axdc4lem  10440  nqereu  10915  mulcanenq  10946  archnq  10966  prlem934  11019  supsrlem  11097  supsr  11098  swrdccatin1  14764  swrdccat3blem  14778  fsum2dlem  15823  fprod2dlem  16036  vdwlem10  17051  imasaddfnlem  17583  catideu  17732  iscatd2  17738  catlid  17740  catpropd  17766  symg2bas  19464  efgmval  19783  efgi  19790  vrgpval  19838  gsumcom2  20046  rngqiprngimfo  21422  pzriprnglem10  21621  pzriprnglem11  21622  txkgen  23790  cnmpt21  23809  xkoinjcn  23825  txconn  23827  pt1hmeo  23944  cnextfvval  24203  qustgplem  24259  dvbsss  26042  axlowdim2  29291  axlowdim  29292  axcontlem10  29304  axcontlem12  29306  isnvlem  30943  br8d  32934  2ndresdju  32975  gsumhashmul  33368  gsumwrd2dccatlem  33378  rlocf1  33575  idomsubr  33611  prsrn  34286  esum2dlem  34463  eulerpartlemgvv  34747  fineqvrep  35508  satf0op  35850  satffunlem1lem1  35875  satffunlem2lem1  35877  sategoelfvb  35892  br8  36229  br6  36230  br4  36231  eldm3  36234  dfdm5  36246  elfuns  36386  brimg  36408  brapply  36409  lemsuccf  36412  brrestrict  36422  dfrdg4  36424  cgrdegen  36477  brofs  36478  cgrextend  36481  brifs  36516  ifscgr  36517  brcgr3  36519  brcolinear2  36531  colineardim1  36534  brfs  36552  idinside  36557  btwnconn1lem7  36566  btwnconn1lem11  36570  btwnconn1lem12  36571  brsegle  36581  outsideofeu  36604  fvray  36614  linedegen  36616  fvline  36617  cbvoprab1vw  36730  cbvoprab13vw  36734  cbvopab1davw  36757  cbvoprab1davw  36764  bj-inftyexpiinv  37833  bj-inftyexpidisj  37835  finxpeq2  38014  finxpreclem6  38023  finxpsuclem  38024  curfv  38232  isdivrngo  38582  drngoi  38583  dicelval3  41935  dihjatcclem4  42176  dropab1  45139  relopabVD  45592  funressndmafv2rn  47943  dfatdmfcoafv2  47974  ichnreuop  48204  ichreuopeq  48205  reuopreuprim  48258  gpgedgvtx0  48809  gpgedgvtx1  48810  gpgcubic  48827  gpg5nbgr3star  48829  pgnbgreunbgrlem3  48866  pgnbgreunbgrlem6  48872  pgnbgreunbgr  48873  sectpropdlem  49797  ssccatid  49833  upfval2  49938  isthincd2lem2  50196