Theorem opeq2 4874

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 2822	. . . 4 ⊢ (𝐴 = 𝐵 → (𝐴 ∈ V ↔ 𝐵 ∈ V))
2	1	anbi2d 630	. . 3 ⊢ (𝐴 = 𝐵 → ((𝐶 ∈ V ∧ 𝐴 ∈ V) ↔ (𝐶 ∈ V ∧ 𝐵 ∈ V)))
3		preq2 4738	. . . 4 ⊢ (𝐴 = 𝐵 → {𝐶, 𝐴} = {𝐶, 𝐵})
4	3	preq2d 4744	. . 3 ⊢ (𝐴 = 𝐵 → {{𝐶}, {𝐶, 𝐴}} = {{𝐶}, {𝐶, 𝐵}})
5	2, 4	ifbieq1d 4552	. 2 ⊢ (𝐴 = 𝐵 → if((𝐶 ∈ V ∧ 𝐴 ∈ V), {{𝐶}, {𝐶, 𝐴}}, ∅) = if((𝐶 ∈ V ∧ 𝐵 ∈ V), {{𝐶}, {𝐶, 𝐵}}, ∅))
6		dfopif 4870	. 2 ⊢ ⟨𝐶, 𝐴⟩ = if((𝐶 ∈ V ∧ 𝐴 ∈ V), {{𝐶}, {𝐶, 𝐴}}, ∅)
7		dfopif 4870	. 2 ⊢ ⟨𝐶, 𝐵⟩ = if((𝐶 ∈ V ∧ 𝐵 ∈ V), {{𝐶}, {𝐶, 𝐵}}, ∅)
8	5, 6, 7	3eqtr4g 2798	1 ⊢ (𝐴 = 𝐵 → ⟨𝐶, 𝐴⟩ = ⟨𝐶, 𝐵⟩)

Syntax hints:   → wi 4   ∧ wa 397   = wceq 1542   ∈ wcel 2107  Vcvv 3475  ∅c0 4322  ifcif 4528  {csn 4628  {cpr 4630  ⟨cop 4634

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3434  df-v 3477  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635

This theorem is referenced by:  opeq12  4875  opeq2i  4877  opeq2d  4880  oteq2  4883  oteq3  4884  breq2  5152  cbvopab2  5225  cbvopab2v  5229  opthg  5477  eqvinop  5487  opelopabsb  5530  dfid3  5577  opelxp  5712  relopabi  5821  opabid2  5827  elrn2g  5889  opeldmd  5905  opeldm  5906  iss  6034  elidinxp  6042  elimasngOLD  6087  dmsnopg  6210  reuop  6290  funopg  6580  f1osng  6872  f1oprswap  6875  tz6.12f  6915  fvn0ssdmfun  7074  fsn  7130  fsng  7132  fprg  7150  fprb  7192  oveq2  7414  cbvoprab2  7494  ovg  7569  elxp4  7910  elxp5  7911  opabex3d  7949  opabex3rd  7950  opabex3  7951  op1stg  7984  op2ndg  7985  op1steq  8016  dfoprab4f  8039  fsplit  8100  xpord2pred  8128  seqomlem2  8448  omeu  8582  oeeui  8599  ralxpmap  8887  elixpsn  8928  ixpsnf1o  8929  mapsnend  9033  xpsnen  9052  xpassen  9063  xpf1o  9136  unxpdomlem1  9247  djulcl  9902  djurcl  9903  djur  9911  djuss  9912  djuun  9918  1stinl  9919  2ndinl  9920  1stinr  9921  2ndinr  9922  axdc4lem  10447  nqereu  10921  mulcanenq  10952  elreal  11123  ax1rid  11153  fseq1p1m1  13572  pfxval  14620  swrdccatin1  14672  swrdccat3blem  14686  wrdlen2  14892  ruclem1  16171  imasaddfnlem  17471  imasvscafn  17480  catidex  17615  catpropd  17650  funcsetcestrclem1  18103  symg2bas  19255  efgi  19582  gsumcom2  19838  mat1rhmval  21973  mat1ric  21981  txkgen  23148  cnmpt21  23167  xkoinjcn  23183  txconn  23185  xpstopnlem1  23305  qustgplem  23617  metustid  24055  axlowdim2  28208  axlowdim  28209  axcontlem2  28213  axcontlem3  28214  axcontlem4  28215  axcontlem9  28220  axcontlem10  28221  axcontlem11  28222  cusgrexg  28691  rgrusgrprc  28836  2clwwlk2clwwlk  29593  isnvlem  29851  br8d  31827  gsumhashmul  32196  prsdm  32883  eulerpartlemgvv  33364  reprsuc  33616  bnj941  33772  bnj944  33938  fineqvrep  34084  cvmlift2lem1  34282  cvmlift2lem12  34294  goel  34327  gonafv  34330  satf0op  34357  sat1el2xp  34359  fmla0xp  34363  sategoelfvb  34399  br8  34715  br6  34716  br4  34717  dfrn5  34734  elima4  34736  pprodss4v  34845  brimg  34898  brapply  34899  brsuccf  34902  brrestrict  34910  dfrdg4  34912  cgrtriv  34963  brofs  34966  segconeu  34972  btwntriv2  34973  transportprops  34995  brifs  35004  ifscgr  35005  brcgr3  35007  cgrxfr  35016  brcolinear2  35019  colineardim1  35022  brfs  35040  idinside  35045  btwnconn1lem7  35054  btwnconn1lem11  35058  btwnconn1lem12  35059  btwnconn1lem14  35061  brsegle  35069  seglerflx  35073  seglemin  35074  segleantisym  35076  btwnsegle  35078  outsideofeu  35092  outsidele  35093  linedegen  35104  fvline  35105  finxpreclem6  36266  finxpsuclem  36267  curfv  36457  poimirlem4  36481  poimirlem26  36503  isdivrngo  36807  drngoi  36808  iss2  37202  dibelval3  40007  diblsmopel  40031  dihjatcclem4  40281  frlmsnic  41108  dfhe3  42512  dffrege115  42715  dropab2  43193  relopabVD  43648  projf1o  43882  sge0xp  45132  hoidmv1le  45297  fsetsniunop  45746  fsetsnf  45748  fsetsnf1  45749  fsetsnfo  45750  ichnreuop  46127  ichreuopeq  46128  reuopreuprim  46181  0aryfvalel  47274  1arymaptf1  47282  2arymaptf1  47293  prelrrx2b  47354  rrx2xpref1o  47358  rrx2plordisom  47363  isthincd2lem2  47610