Theorem opeq2 4834

Description: Equality theorem for ordered pairs. (Contributed by NM, 25-Jun-1998.) (Revised by Mario Carneiro, 26-Apr-2015.)

Assertion

Ref	Expression
opeq2	⊢ (𝐴 = 𝐵 → ⟨𝐶, 𝐴⟩ = ⟨𝐶, 𝐵⟩)

Proof of Theorem opeq2

Step	Hyp	Ref	Expression
1		eleq1 2848	. . . 4 ⊢ (𝐴 = 𝐵 → (𝐴 ∈ V ↔ 𝐵 ∈ V))
2	1	anbi2d 642	. . 3 ⊢ (𝐴 = 𝐵 → ((𝐶 ∈ V ∧ 𝐴 ∈ V) ↔ (𝐶 ∈ V ∧ 𝐵 ∈ V)))
3		preq2 4695	. . . 4 ⊢ (𝐴 = 𝐵 → {𝐶, 𝐴} = {𝐶, 𝐵})
4	3	preq2d 4701	. . 3 ⊢ (𝐴 = 𝐵 → {{𝐶}, {𝐶, 𝐴}} = {{𝐶}, {𝐶, 𝐵}})
5	2, 4	ifbieq1d 4507	. 2 ⊢ (𝐴 = 𝐵 → if((𝐶 ∈ V ∧ 𝐴 ∈ V), {{𝐶}, {𝐶, 𝐴}}, ∅) = if((𝐶 ∈ V ∧ 𝐵 ∈ V), {{𝐶}, {𝐶, 𝐵}}, ∅))
6		dfopif 4830	. 2 ⊢ ⟨𝐶, 𝐴⟩ = if((𝐶 ∈ V ∧ 𝐴 ∈ V), {{𝐶}, {𝐶, 𝐴}}, ∅)
7		dfopif 4830	. 2 ⊢ ⟨𝐶, 𝐵⟩ = if((𝐶 ∈ V ∧ 𝐵 ∈ V), {{𝐶}, {𝐶, 𝐵}}, ∅)
8	5, 6, 7	3eqtr4g 2820	1 ⊢ (𝐴 = 𝐵 → ⟨𝐶, 𝐴⟩ = ⟨𝐶, 𝐵⟩)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570   ∈ wcel 2145  Vcvv 3450  ∅c0 4279  ifcif 4482  {csn 4584  {cpr 4586  ⟨cop 4590

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591

This theorem is used by:  opeq12  4835  opeq2i  4837  opeq2d  4840  oteq2  4843  oteq3  4844  breq2  5107  cbvopab2  5181  cbvopab2v  5184  opthg  5453  eqvinop  5463  opelopabsb  5508  dfid3  5553  opelxp  5691  relopabi  5803  opabid2  5809  elrn2g  5874  opeldmd  5890  opeldm  5891  iss  6031  elidinxp  6040  dmsnopg  6209  reuop  6291  funopg  6567  f1osng  6860  f1oprswap  6863  tz6.12f  6903  fvn0ssdmfun  7067  fsn  7129  fsng  7131  fprg  7152  fprb  7192  oveq2  7421  cbvoprab2  7501  cbvoprab3v  7505  ovg  7578  elxp4  7919  elxp5  7920  opabex3d  7962  opabex3rd  7963  opabex3  7964  op1stg  7998  op2ndg  7999  op1steq  8030  dfoprab4f  8053  fsplit  8114  xpord2pred  8143  seqomlem2  8440  omeu  8572  oeeui  8590  curfv  8871  ralxpmap  8903  elixpsn  8944  ixpsnf1o  8945  mapsnend  9043  xpsnen  9059  xpassen  9069  xpf1o  9137  unxpdomlem1  9226  djulcl  9915  djurcl  9916  djur  9924  djuss  9925  djuun  9931  1stinl  9932  2ndinl  9933  1stinr  9934  2ndinr  9935  axdc4lem  10457  nqereu  10938  mulcanenq  10969  elreal  11140  ax1rid  11170  fseq1p1m1  13653  pfxval  14743  swrdccatin1  14794  swrdccat3blem  14808  wrdlen2  15015  ruclem1  16319  imasaddfnlem  17614  imasvscafn  17623  catidex  17762  catpropd  17797  funcsetcestrclem1  18242  degenmgm  19050  degenmgm2nfun  19052  degenmgm2  19053  symg2bas  19520  efgi  19846  gsumcom2  20102  pzriprnglem3  21696  pzriprnglem10  21703  mat1rhmval  22701  mat1ric  22709  txkgen  23878  cnmpt21  23897  xkoinjcn  23913  txconn  23915  xpstopnlem1  24035  qustgplem  24347  metustid  24780  angmgmval  29273  axlowdim2  29417  axlowdim  29418  axcontlem2  29422  axcontlem3  29423  axcontlem4  29424  axcontlem9  29429  axcontlem10  29430  axcontlem11  29431  cusgrexg  29904  rgrusgrprc  30049  2clwwlk2clwwlk  30830  isnvlem  31091  br8d  33081  gsumhashmul  33507  prsdm  34424  eulerpartlemgvv  34887  reprsuc  35123  bnj941  35282  bnj944  35447  fineqvrep  35640  cvmlift2lem1  35881  cvmlift2lem12  35893  goel  35926  gonafv  35929  satf0op  35956  sat1el2xp  35958  fmla0xp  35962  sategoelfvb  35998  br8  36335  br6  36336  br4  36337  dfrn5  36353  elima4  36355  pprodss4v  36461  brimg  36514  brapply  36515  lemsuccf  36518  brrestrict  36528  dfrdg4  36530  cgrtriv  36582  brofs  36585  segconeu  36591  btwntriv2  36592  transportprops  36614  brifs  36623  ifscgr  36624  brcgr3  36626  cgrxfr  36635  brcolinear2  36638  colineardim1  36641  brfs  36659  idinside  36664  btwnconn1lem7  36673  btwnconn1lem11  36677  btwnconn1lem12  36678  btwnconn1lem14  36680  brsegle  36688  seglerflx  36692  seglemin  36693  segleantisym  36695  btwnsegle  36697  outsideofeu  36711  outsidele  36712  linedegen  36723  fvline  36724  cbvoprab2vw  36858  cbvoprab23vw  36860  cbvopab2davw  36885  cbvoprab2davw  36892  finxpreclem6  38150  finxpsuclem  38151  poimirlem4  38373  poimirlem26  38395  isdivrngo  38700  drngoi  38701  iss2  39092  dibelval3  42020  diblsmopel  42044  dihjatcclem4  42294  frlmsnic  43422  dfhe3  44615  dffrege115  44818  dropab2  45271  relopabVD  45723  projf1o  46028  sge0xp  47257  hoidmv1le  47422  fsetsniunop  47937  fsetsnf  47939  fsetsnf1  47940  fsetsnfo  47941  ichnreuop  48372  ichreuopeq  48373  reuopreuprim  48426  gpgprismgriedgdmss  48968  gpgvtx0  48969  gpgvtx1  48970  gpgedgvtx0  48977  gpgedgvtx1  48978  gpgedgiov  48981  gpgedg2ov  48982  gpgedg2iv  48983  gpg3kgrtriexlem6  49004  gpgprismgr4cycllem3  49013  pgnbgreunbgrlem1  49029  pgnbgreunbgrlem2  49033  pgnbgreunbgrlem4  49035  pgnbgreunbgrlem5lem1  49036  pgnbgreunbgrlem5lem2  49037  pgnbgreunbgrlem5lem3  49038  pgnbgreunbgrlem5  49039  gpg5edgnedg  49046  0aryfvalel  49564  1arymaptf1  49572  2arymaptf1  49583  prelrrx2b  49644  rrx2xpref1o  49648  rrx2plordisom  49653  sectpropdlem  49962  ssccatid  49998  isthincd2lem2  50361