Theorem opeq2 4832

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 2825	. . . 4 ⊢ (𝐴 = 𝐵 → (𝐴 ∈ V ↔ 𝐵 ∈ V))
2	1	anbi2d 631	. . 3 ⊢ (𝐴 = 𝐵 → ((𝐶 ∈ V ∧ 𝐴 ∈ V) ↔ (𝐶 ∈ V ∧ 𝐵 ∈ V)))
3		preq2 4693	. . . 4 ⊢ (𝐴 = 𝐵 → {𝐶, 𝐴} = {𝐶, 𝐵})
4	3	preq2d 4699	. . 3 ⊢ (𝐴 = 𝐵 → {{𝐶}, {𝐶, 𝐴}} = {{𝐶}, {𝐶, 𝐵}})
5	2, 4	ifbieq1d 4506	. 2 ⊢ (𝐴 = 𝐵 → if((𝐶 ∈ V ∧ 𝐴 ∈ V), {{𝐶}, {𝐶, 𝐴}}, ∅) = if((𝐶 ∈ V ∧ 𝐵 ∈ V), {{𝐶}, {𝐶, 𝐵}}, ∅))
6		dfopif 4828	. 2 ⊢ ⟨𝐶, 𝐴⟩ = if((𝐶 ∈ V ∧ 𝐴 ∈ V), {{𝐶}, {𝐶, 𝐴}}, ∅)
7		dfopif 4828	. 2 ⊢ ⟨𝐶, 𝐵⟩ = if((𝐶 ∈ V ∧ 𝐵 ∈ V), {{𝐶}, {𝐶, 𝐵}}, ∅)
8	5, 6, 7	3eqtr4g 2797	1 ⊢ (𝐴 = 𝐵 → ⟨𝐶, 𝐴⟩ = ⟨𝐶, 𝐵⟩)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1542   ∈ wcel 2114  Vcvv 3442  ∅c0 4287  ifcif 4481  {csn 4582  {cpr 4584  ⟨cop 4588

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589

This theorem is referenced by:  opeq12  4833  opeq2i  4835  opeq2d  4838  oteq2  4841  oteq3  4842  breq2  5104  cbvopab2  5176  cbvopab2v  5179  opthg  5433  eqvinop  5443  opelopabsb  5486  dfid3  5530  opelxp  5668  relopabi  5779  opabid2  5785  elrn2g  5847  opeldmd  5863  opeldm  5864  iss  6002  elidinxp  6011  dmsnopg  6179  reuop  6259  funopg  6534  f1osng  6824  f1oprswap  6827  tz6.12f  6867  fvn0ssdmfun  7028  fsn  7090  fsng  7092  fprg  7110  fprb  7150  oveq2  7376  cbvoprab2  7456  cbvoprab3v  7460  ovg  7533  elxp4  7874  elxp5  7875  opabex3d  7919  opabex3rd  7920  opabex3  7921  op1stg  7955  op2ndg  7956  op1steq  7987  dfoprab4f  8010  fsplit  8069  xpord2pred  8097  seqomlem2  8392  omeu  8522  oeeui  8540  ralxpmap  8846  elixpsn  8887  ixpsnf1o  8888  mapsnend  8985  xpsnen  9001  xpassen  9011  xpf1o  9079  unxpdomlem1  9168  djulcl  9834  djurcl  9835  djur  9843  djuss  9844  djuun  9850  1stinl  9851  2ndinl  9852  1stinr  9853  2ndinr  9854  axdc4lem  10377  nqereu  10852  mulcanenq  10883  elreal  11054  ax1rid  11084  fseq1p1m1  13526  pfxval  14609  swrdccatin1  14660  swrdccat3blem  14674  wrdlen2  14879  ruclem1  16168  imasaddfnlem  17461  imasvscafn  17470  catidex  17609  catpropd  17644  funcsetcestrclem1  18089  symg2bas  19334  efgi  19660  gsumcom2  19916  pzriprnglem3  21450  pzriprnglem10  21457  mat1rhmval  22435  mat1ric  22443  txkgen  23608  cnmpt21  23627  xkoinjcn  23643  txconn  23645  xpstopnlem1  23765  qustgplem  24077  metustid  24510  axlowdim2  29045  axlowdim  29046  axcontlem2  29050  axcontlem3  29051  axcontlem4  29052  axcontlem9  29057  axcontlem10  29058  axcontlem11  29059  cusgrexg  29529  rgrusgrprc  29675  2clwwlk2clwwlk  30437  isnvlem  30698  br8d  32698  gsumhashmul  33161  prsdm  34092  eulerpartlemgvv  34554  reprsuc  34793  bnj941  34949  bnj944  35114  fineqvrep  35292  cvmlift2lem1  35518  cvmlift2lem12  35530  goel  35563  gonafv  35566  satf0op  35593  sat1el2xp  35595  fmla0xp  35599  sategoelfvb  35635  br8  35972  br6  35973  br4  35974  dfrn5  35990  elima4  35992  pprodss4v  36098  brimg  36151  brapply  36152  lemsuccf  36155  brrestrict  36165  dfrdg4  36167  cgrtriv  36218  brofs  36221  segconeu  36227  btwntriv2  36228  transportprops  36250  brifs  36259  ifscgr  36260  brcgr3  36262  cgrxfr  36271  brcolinear2  36274  colineardim1  36277  brfs  36295  idinside  36300  btwnconn1lem7  36309  btwnconn1lem11  36313  btwnconn1lem12  36314  btwnconn1lem14  36316  brsegle  36324  seglerflx  36328  seglemin  36329  segleantisym  36331  btwnsegle  36333  outsideofeu  36347  outsidele  36348  linedegen  36359  fvline  36360  cbvoprab2vw  36454  cbvoprab23vw  36456  cbvopab2davw  36481  cbvoprab2davw  36488  finxpreclem6  37651  finxpsuclem  37652  curfv  37851  poimirlem4  37875  poimirlem26  37897  isdivrngo  38201  drngoi  38202  iss2  38595  dibelval3  41523  diblsmopel  41547  dihjatcclem4  41797  frlmsnic  42910  dfhe3  44131  dffrege115  44334  dropab2  44803  relopabVD  45256  projf1o  45555  sge0xp  46787  hoidmv1le  46952  fsetsniunop  47409  fsetsnf  47411  fsetsnf1  47412  fsetsnfo  47413  ichnreuop  47832  ichreuopeq  47833  reuopreuprim  47886  gpgprismgriedgdmss  48412  gpgvtx0  48413  gpgvtx1  48414  gpgedgvtx0  48421  gpgedgvtx1  48422  gpgedgiov  48425  gpgedg2ov  48426  gpgedg2iv  48427  gpg3kgrtriexlem6  48448  gpgprismgr4cycllem3  48457  pgnbgreunbgrlem1  48473  pgnbgreunbgrlem2  48477  pgnbgreunbgrlem4  48479  pgnbgreunbgrlem5lem1  48480  pgnbgreunbgrlem5lem2  48481  pgnbgreunbgrlem5lem3  48482  pgnbgreunbgrlem5  48483  gpg5edgnedg  48490  0aryfvalel  48994  1arymaptf1  49002  2arymaptf1  49013  prelrrx2b  49074  rrx2xpref1o  49078  rrx2plordisom  49083  sectpropdlem  49395  ssccatid  49431  isthincd2lem2  49794