Theorem opeq2 4875

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 2819	. . . 4 ⊢ (𝐴 = 𝐵 → (𝐴 ∈ V ↔ 𝐵 ∈ V))
2	1	anbi2d 627	. . 3 ⊢ (𝐴 = 𝐵 → ((𝐶 ∈ V ∧ 𝐴 ∈ V) ↔ (𝐶 ∈ V ∧ 𝐵 ∈ V)))
3		preq2 4739	. . . 4 ⊢ (𝐴 = 𝐵 → {𝐶, 𝐴} = {𝐶, 𝐵})
4	3	preq2d 4745	. . 3 ⊢ (𝐴 = 𝐵 → {{𝐶}, {𝐶, 𝐴}} = {{𝐶}, {𝐶, 𝐵}})
5	2, 4	ifbieq1d 4553	. 2 ⊢ (𝐴 = 𝐵 → if((𝐶 ∈ V ∧ 𝐴 ∈ V), {{𝐶}, {𝐶, 𝐴}}, ∅) = if((𝐶 ∈ V ∧ 𝐵 ∈ V), {{𝐶}, {𝐶, 𝐵}}, ∅))
6		dfopif 4871	. 2 ⊢ ⟨𝐶, 𝐴⟩ = if((𝐶 ∈ V ∧ 𝐴 ∈ V), {{𝐶}, {𝐶, 𝐴}}, ∅)
7		dfopif 4871	. 2 ⊢ ⟨𝐶, 𝐵⟩ = if((𝐶 ∈ V ∧ 𝐵 ∈ V), {{𝐶}, {𝐶, 𝐵}}, ∅)
8	5, 6, 7	3eqtr4g 2795	1 ⊢ (𝐴 = 𝐵 → ⟨𝐶, 𝐴⟩ = ⟨𝐶, 𝐵⟩)

Syntax hints:   → wi 4   ∧ wa 394   = wceq 1539   ∈ wcel 2104  Vcvv 3472  ∅c0 4323  ifcif 4529  {csn 4629  {cpr 4631  ⟨cop 4635

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-rab 3431  df-v 3474  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636

This theorem is referenced by:  opeq12  4876  opeq2i  4878  opeq2d  4881  oteq2  4884  oteq3  4885  breq2  5153  cbvopab2  5226  cbvopab2v  5230  opthg  5478  eqvinop  5488  opelopabsb  5531  dfid3  5578  opelxp  5713  relopabi  5823  opabid2  5829  elrn2g  5891  opeldmd  5907  opeldm  5908  iss  6036  elidinxp  6044  elimasngOLD  6090  dmsnopg  6213  reuop  6293  funopg  6583  f1osng  6875  f1oprswap  6878  tz6.12f  6918  fvn0ssdmfun  7077  fsn  7136  fsng  7138  fprg  7156  fprb  7198  oveq2  7421  cbvoprab2  7501  ovg  7576  elxp4  7917  elxp5  7918  opabex3d  7956  opabex3rd  7957  opabex3  7958  op1stg  7991  op2ndg  7992  op1steq  8023  dfoprab4f  8046  fsplit  8107  xpord2pred  8135  seqomlem2  8455  omeu  8589  oeeui  8606  ralxpmap  8894  elixpsn  8935  ixpsnf1o  8936  mapsnend  9040  xpsnen  9059  xpassen  9070  xpf1o  9143  unxpdomlem1  9254  djulcl  9909  djurcl  9910  djur  9918  djuss  9919  djuun  9925  1stinl  9926  2ndinl  9927  1stinr  9928  2ndinr  9929  axdc4lem  10454  nqereu  10928  mulcanenq  10959  elreal  11130  ax1rid  11160  fseq1p1m1  13581  pfxval  14629  swrdccatin1  14681  swrdccat3blem  14695  wrdlen2  14901  ruclem1  16180  imasaddfnlem  17480  imasvscafn  17489  catidex  17624  catpropd  17659  funcsetcestrclem1  18112  symg2bas  19303  efgi  19630  gsumcom2  19886  pzriprnglem3  21254  pzriprnglem10  21261  mat1rhmval  22203  mat1ric  22211  txkgen  23378  cnmpt21  23397  xkoinjcn  23413  txconn  23415  xpstopnlem1  23535  qustgplem  23847  metustid  24285  axlowdim2  28483  axlowdim  28484  axcontlem2  28488  axcontlem3  28489  axcontlem4  28490  axcontlem9  28495  axcontlem10  28496  axcontlem11  28497  cusgrexg  28966  rgrusgrprc  29111  2clwwlk2clwwlk  29868  isnvlem  30128  br8d  32104  gsumhashmul  32476  prsdm  33190  eulerpartlemgvv  33671  reprsuc  33923  bnj941  34079  bnj944  34245  fineqvrep  34391  cvmlift2lem1  34589  cvmlift2lem12  34601  goel  34634  gonafv  34637  satf0op  34664  sat1el2xp  34666  fmla0xp  34670  sategoelfvb  34706  br8  35028  br6  35029  br4  35030  dfrn5  35047  elima4  35049  pprodss4v  35158  brimg  35211  brapply  35212  brsuccf  35215  brrestrict  35223  dfrdg4  35225  cgrtriv  35276  brofs  35279  segconeu  35285  btwntriv2  35286  transportprops  35308  brifs  35317  ifscgr  35318  brcgr3  35320  cgrxfr  35329  brcolinear2  35332  colineardim1  35335  brfs  35353  idinside  35358  btwnconn1lem7  35367  btwnconn1lem11  35371  btwnconn1lem12  35372  btwnconn1lem14  35374  brsegle  35382  seglerflx  35386  seglemin  35387  segleantisym  35389  btwnsegle  35391  outsideofeu  35405  outsidele  35406  linedegen  35417  fvline  35418  finxpreclem6  36582  finxpsuclem  36583  curfv  36773  poimirlem4  36797  poimirlem26  36819  isdivrngo  37123  drngoi  37124  iss2  37518  dibelval3  40323  diblsmopel  40347  dihjatcclem4  40597  frlmsnic  41414  dfhe3  42830  dffrege115  43033  dropab2  43511  relopabVD  43966  projf1o  44196  sge0xp  45445  hoidmv1le  45610  fsetsniunop  46059  fsetsnf  46061  fsetsnf1  46062  fsetsnfo  46063  ichnreuop  46440  ichreuopeq  46441  reuopreuprim  46494  0aryfvalel  47409  1arymaptf1  47417  2arymaptf1  47428  prelrrx2b  47489  rrx2xpref1o  47493  rrx2plordisom  47498  isthincd2lem2  47745