Theorem opeq2 4898

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 2832	. . . 4 ⊢ (𝐴 = 𝐵 → (𝐴 ∈ V ↔ 𝐵 ∈ V))
2	1	anbi2d 629	. . 3 ⊢ (𝐴 = 𝐵 → ((𝐶 ∈ V ∧ 𝐴 ∈ V) ↔ (𝐶 ∈ V ∧ 𝐵 ∈ V)))
3		preq2 4759	. . . 4 ⊢ (𝐴 = 𝐵 → {𝐶, 𝐴} = {𝐶, 𝐵})
4	3	preq2d 4765	. . 3 ⊢ (𝐴 = 𝐵 → {{𝐶}, {𝐶, 𝐴}} = {{𝐶}, {𝐶, 𝐵}})
5	2, 4	ifbieq1d 4572	. 2 ⊢ (𝐴 = 𝐵 → if((𝐶 ∈ V ∧ 𝐴 ∈ V), {{𝐶}, {𝐶, 𝐴}}, ∅) = if((𝐶 ∈ V ∧ 𝐵 ∈ V), {{𝐶}, {𝐶, 𝐵}}, ∅))
6		dfopif 4894	. 2 ⊢ ⟨𝐶, 𝐴⟩ = if((𝐶 ∈ V ∧ 𝐴 ∈ V), {{𝐶}, {𝐶, 𝐴}}, ∅)
7		dfopif 4894	. 2 ⊢ ⟨𝐶, 𝐵⟩ = if((𝐶 ∈ V ∧ 𝐵 ∈ V), {{𝐶}, {𝐶, 𝐵}}, ∅)
8	5, 6, 7	3eqtr4g 2805	1 ⊢ (𝐴 = 𝐵 → ⟨𝐶, 𝐴⟩ = ⟨𝐶, 𝐵⟩)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1537   ∈ wcel 2108  Vcvv 3488  ∅c0 4352  ifcif 4548  {csn 4648  {cpr 4650  ⟨cop 4654

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655

This theorem is referenced by:  opeq12  4899  opeq2i  4901  opeq2d  4904  oteq2  4907  oteq3  4908  breq2  5170  cbvopab2  5243  cbvopab2v  5247  opthg  5497  eqvinop  5507  opelopabsb  5549  dfid3  5596  opelxp  5736  relopabi  5846  opabid2  5852  elrn2g  5915  opeldmd  5931  opeldm  5932  iss  6064  elidinxp  6073  elimasngOLD  6120  dmsnopg  6244  reuop  6324  funopg  6612  f1osng  6903  f1oprswap  6906  tz6.12f  6946  fvn0ssdmfun  7108  fsn  7169  fsng  7171  fprg  7189  fprb  7231  oveq2  7456  cbvoprab2  7538  cbvoprab3v  7542  ovg  7615  elxp4  7962  elxp5  7963  opabex3d  8006  opabex3rd  8007  opabex3  8008  op1stg  8042  op2ndg  8043  op1steq  8074  dfoprab4f  8097  fsplit  8158  xpord2pred  8186  seqomlem2  8507  omeu  8641  oeeui  8658  ralxpmap  8954  elixpsn  8995  ixpsnf1o  8996  mapsnend  9101  xpsnen  9121  xpassen  9132  xpf1o  9205  unxpdomlem1  9313  djulcl  9979  djurcl  9980  djur  9988  djuss  9989  djuun  9995  1stinl  9996  2ndinl  9997  1stinr  9998  2ndinr  9999  axdc4lem  10524  nqereu  10998  mulcanenq  11029  elreal  11200  ax1rid  11230  fseq1p1m1  13658  pfxval  14721  swrdccatin1  14773  swrdccat3blem  14787  wrdlen2  14993  ruclem1  16279  imasaddfnlem  17588  imasvscafn  17597  catidex  17732  catpropd  17767  funcsetcestrclem1  18223  symg2bas  19434  efgi  19761  gsumcom2  20017  pzriprnglem3  21517  pzriprnglem10  21524  mat1rhmval  22506  mat1ric  22514  txkgen  23681  cnmpt21  23700  xkoinjcn  23716  txconn  23718  xpstopnlem1  23838  qustgplem  24150  metustid  24588  axlowdim2  28993  axlowdim  28994  axcontlem2  28998  axcontlem3  28999  axcontlem4  29000  axcontlem9  29005  axcontlem10  29006  axcontlem11  29007  cusgrexg  29479  rgrusgrprc  29625  2clwwlk2clwwlk  30382  isnvlem  30642  br8d  32632  gsumhashmul  33040  prsdm  33860  eulerpartlemgvv  34341  reprsuc  34592  bnj941  34748  bnj944  34914  fineqvrep  35071  cvmlift2lem1  35270  cvmlift2lem12  35282  goel  35315  gonafv  35318  satf0op  35345  sat1el2xp  35347  fmla0xp  35351  sategoelfvb  35387  br8  35718  br6  35719  br4  35720  dfrn5  35737  elima4  35739  pprodss4v  35848  brimg  35901  brapply  35902  brsuccf  35905  brrestrict  35913  dfrdg4  35915  cgrtriv  35966  brofs  35969  segconeu  35975  btwntriv2  35976  transportprops  35998  brifs  36007  ifscgr  36008  brcgr3  36010  cgrxfr  36019  brcolinear2  36022  colineardim1  36025  brfs  36043  idinside  36048  btwnconn1lem7  36057  btwnconn1lem11  36061  btwnconn1lem12  36062  btwnconn1lem14  36064  brsegle  36072  seglerflx  36076  seglemin  36077  segleantisym  36079  btwnsegle  36081  outsideofeu  36095  outsidele  36096  linedegen  36107  fvline  36108  cbvoprab2vw  36204  cbvoprab23vw  36206  cbvopab2davw  36231  cbvoprab2davw  36238  finxpreclem6  37362  finxpsuclem  37363  curfv  37560  poimirlem4  37584  poimirlem26  37606  isdivrngo  37910  drngoi  37911  iss2  38300  dibelval3  41104  diblsmopel  41128  dihjatcclem4  41378  frlmsnic  42495  dfhe3  43737  dffrege115  43940  dropab2  44417  relopabVD  44872  projf1o  45104  sge0xp  46350  hoidmv1le  46515  fsetsniunop  46964  fsetsnf  46966  fsetsnf1  46967  fsetsnfo  46968  ichnreuop  47346  ichreuopeq  47347  reuopreuprim  47400  0aryfvalel  48368  1arymaptf1  48376  2arymaptf1  48387  prelrrx2b  48448  rrx2xpref1o  48452  rrx2plordisom  48457  isthincd2lem2  48703