Theorem opeq2 4843

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 2857	. . . 4 ⊢ (𝐴 = 𝐵 → (𝐴 ∈ V ↔ 𝐵 ∈ V))
2	1	anbi2d 641	. . 3 ⊢ (𝐴 = 𝐵 → ((𝐶 ∈ V ∧ 𝐴 ∈ V) ↔ (𝐶 ∈ V ∧ 𝐵 ∈ V)))
3		preq2 4705	. . . 4 ⊢ (𝐴 = 𝐵 → {𝐶, 𝐴} = {𝐶, 𝐵})
4	3	preq2d 4711	. . 3 ⊢ (𝐴 = 𝐵 → {{𝐶}, {𝐶, 𝐴}} = {{𝐶}, {𝐶, 𝐵}})
5	2, 4	ifbieq1d 4517	. 2 ⊢ (𝐴 = 𝐵 → if((𝐶 ∈ V ∧ 𝐴 ∈ V), {{𝐶}, {𝐶, 𝐴}}, ∅) = if((𝐶 ∈ V ∧ 𝐵 ∈ V), {{𝐶}, {𝐶, 𝐵}}, ∅))
6		dfopif 4839	. 2 ⊢ ⟨𝐶, 𝐴⟩ = if((𝐶 ∈ V ∧ 𝐴 ∈ V), {{𝐶}, {𝐶, 𝐴}}, ∅)
7		dfopif 4839	. 2 ⊢ ⟨𝐶, 𝐵⟩ = if((𝐶 ∈ V ∧ 𝐵 ∈ V), {{𝐶}, {𝐶, 𝐵}}, ∅)
8	5, 6, 7	3eqtr4g 2829	1 ⊢ (𝐴 = 𝐵 → ⟨𝐶, 𝐴⟩ = ⟨𝐶, 𝐵⟩)

Syntax hints:   → wi 4   ∧ wa 400   = wceq 1567   ∈ wcel 2149  Vcvv 3463  ∅c0 4294  ifcif 4492  {csn 4594  {cpr 4596  ⟨cop 4600

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-rab 3424  df-v 3465  df-dif 3916  df-un 3918  df-ss 3930  df-nul 4295  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601

This theorem is referenced by:  opeq12  4844  opeq2i  4846  opeq2d  4849  oteq2  4852  oteq3  4853  breq2  5117  cbvopab2  5191  cbvopab2v  5194  opthg  5460  eqvinop  5470  opelopabsb  5515  dfid3  5560  opelxp  5698  relopabi  5810  opabid2  5816  elrn2g  5881  opeldmd  5897  opeldm  5898  iss  6038  elidinxp  6047  dmsnopg  6215  reuop  6295  funopg  6571  f1osng  6864  f1oprswap  6867  tz6.12f  6907  fvn0ssdmfun  7070  fsn  7132  fsng  7134  fprg  7153  fprb  7193  oveq2  7419  cbvoprab2  7499  cbvoprab3v  7503  ovg  7576  elxp4  7918  elxp5  7919  opabex3d  7961  opabex3rd  7962  opabex3  7963  op1stg  7997  op2ndg  7998  op1steq  8029  dfoprab4f  8052  fsplit  8111  xpord2pred  8140  seqomlem2  8437  omeu  8569  oeeui  8587  ralxpmap  8893  elixpsn  8934  ixpsnf1o  8935  mapsnend  9032  xpsnen  9048  xpassen  9058  xpf1o  9126  unxpdomlem1  9215  djulcl  9895  djurcl  9896  djur  9904  djuss  9905  djuun  9911  1stinl  9912  2ndinl  9913  1stinr  9914  2ndinr  9915  axdc4lem  10438  nqereu  10913  mulcanenq  10944  elreal  11115  ax1rid  11145  fseq1p1m1  13625  pfxval  14710  swrdccatin1  14761  swrdccat3blem  14775  wrdlen2  14980  ruclem1  16286  imasaddfnlem  17581  imasvscafn  17590  catidex  17729  catpropd  17764  funcsetcestrclem1  18209  symg2bas  19462  efgi  19788  gsumcom2  20044  pzriprnglem3  21601  pzriprnglem10  21608  mat1rhmval  22604  mat1ric  22612  txkgen  23777  cnmpt21  23796  xkoinjcn  23812  txconn  23814  xpstopnlem1  23934  qustgplem  24246  metustid  24679  axlowdim2  29250  axlowdim  29251  axcontlem2  29255  axcontlem3  29256  axcontlem4  29257  axcontlem9  29262  axcontlem10  29263  axcontlem11  29264  cusgrexg  29734  rgrusgrprc  29879  2clwwlk2clwwlk  30641  isnvlem  30902  br8d  32893  gsumhashmul  33327  prsdm  34248  eulerpartlemgvv  34710  reprsuc  34946  bnj941  35105  bnj944  35270  fineqvrep  35449  cvmlift2lem1  35692  cvmlift2lem12  35704  goel  35737  gonafv  35740  satf0op  35767  sat1el2xp  35769  fmla0xp  35773  sategoelfvb  35809  br8  36146  br6  36147  br4  36148  dfrn5  36164  elima4  36166  pprodss4v  36272  brimg  36325  brapply  36326  lemsuccf  36329  brrestrict  36339  dfrdg4  36341  cgrtriv  36392  brofs  36395  segconeu  36401  btwntriv2  36402  transportprops  36424  brifs  36433  ifscgr  36434  brcgr3  36436  cgrxfr  36445  brcolinear2  36448  colineardim1  36451  brfs  36469  idinside  36474  btwnconn1lem7  36483  btwnconn1lem11  36487  btwnconn1lem12  36488  btwnconn1lem14  36490  brsegle  36498  seglerflx  36502  seglemin  36503  segleantisym  36505  btwnsegle  36507  outsideofeu  36521  outsidele  36522  linedegen  36533  fvline  36534  cbvoprab2vw  36638  cbvoprab23vw  36640  cbvopab2davw  36665  cbvoprab2davw  36672  finxpreclem6  37929  finxpsuclem  37930  curfv  38138  poimirlem4  38162  poimirlem26  38184  isdivrngo  38488  drngoi  38489  iss2  38882  dibelval3  41810  diblsmopel  41834  dihjatcclem4  42084  frlmsnic  43199  dfhe3  44392  dffrege115  44595  dropab2  45048  relopabVD  45500  projf1o  45805  sge0xp  47034  hoidmv1le  47199  fsetsniunop  47674  fsetsnf  47676  fsetsnf1  47677  fsetsnfo  47678  ichnreuop  48109  ichreuopeq  48110  reuopreuprim  48163  gpgprismgriedgdmss  48705  gpgvtx0  48706  gpgvtx1  48707  gpgedgvtx0  48714  gpgedgvtx1  48715  gpgedgiov  48718  gpgedg2ov  48719  gpgedg2iv  48720  gpg3kgrtriexlem6  48741  gpgprismgr4cycllem3  48750  pgnbgreunbgrlem1  48766  pgnbgreunbgrlem2  48770  pgnbgreunbgrlem4  48772  pgnbgreunbgrlem5lem1  48773  pgnbgreunbgrlem5lem2  48774  pgnbgreunbgrlem5lem3  48775  pgnbgreunbgrlem5  48776  gpg5edgnedg  48783  0aryfvalel  49298  1arymaptf1  49306  2arymaptf1  49317  prelrrx2b  49378  rrx2xpref1o  49382  rrx2plordisom  49387  sectpropdlem  49698  ssccatid  49734  isthincd2lem2  50097