NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  eqeq2d Unicode version

Theorem eqeq2d 2364
Description: Deduction from equality to equivalence of equalities. (Contributed by NM, 27-Dec-1993.)
Hypothesis
Ref Expression
eqeq2d.1
Assertion
Ref Expression
eqeq2d

Proof of Theorem eqeq2d
StepHypRef Expression
1 eqeq2d.1 . 2
2 eqeq2 2362 . 2
31, 2syl 15 1
Colors of variables: wff setvar class
Syntax hints:   wi 4   wb 176   wceq 1642
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-11 1746  ax-ext 2334
This theorem depends on definitions:  df-bi 177  df-ex 1542  df-cleq 2346
This theorem is referenced by:  eqtrd  2385  eq2tri  2412  sbceq1g  3156  euabsn  3792  absneu  3794  unsneqsn  3887  pwadjoin  4119  preqr2g  4126  preq12bg  4128  snel1c  4140  elpw12  4145  elpw11c  4147  elpw121c  4148  elpw131c  4149  elpw141c  4150  elpw151c  4151  elpw161c  4152  elpw171c  4153  elpw181c  4154  elpw191c  4155  elpw1101c  4156  elpw1111c  4157  pw1sn  4165  opkabssvvk  4208  sikexlem  4295  insklem  4304  pw1equn  4331  pw1eqadj  4332  sspw1  4335  sspw12  4336  iotajust  4338  iota1  4353  iota2df  4365  eladdci  4399  addcid1  4405  nnc0suc  4412  elsuc  4413  elsuci  4414  addcass  4415  nnsucelr  4428  opklefing  4448  opkltfing  4449  lefinaddc  4450  preaddccan2lem1  4454  nulge  4456  leltfintr  4458  ltfintr  4459  ltfinp1  4462  lefinlteq  4463  ltfinex  4464  lefinrflx  4467  ltlefin  4468  eqtfinrelk  4486  tfinltfinlem1  4500  0ceven  4505  sucoddeven  4511  evenodddisjlem1  4515  eventfin  4517  oddtfin  4518  nnadjoin  4520  tfinnn  4534  vfinspsslem1  4550  vfinspss  4551  dfphi2  4569  phi11lem1  4595  0cnelphi  4597  eqvinop  4606  phidisjnn  4615  phialllem1  4616  phialllem2  4617  cbvopab  4630  cbvopab1  4632  cbvopab2  4633  cbvopab1s  4634  cbvopab2v  4636  el1st  4729  elswap  4740  dfid3  4768  br1st  4858  br2nd  4859  brswap2  4860  elsnres  4996  elxp4  5108  dfxp2  5113  funcnvuni  5161  iunfopab  5204  fun11iun  5305  dffn5  5363  fvopab4g  5388  foco2  5426  fsng  5433  fconst5  5455  abrexco  5463  dff13f  5472  f1fveq  5473  f1ocnvfv  5478  f1ocnvfvb  5479  f1oiso2  5500  xpnedisj  5513  oprabid  5550  rspceov  5556  dfoprab2  5558  cbvoprab1  5567  cbvoprab2  5568  cbvoprab12  5569  fnov  5591  ov3  5599  ov6g  5600  fnrnov  5605  foov  5606  caovcan  5628  mpteq12f  5655  mpt2eq123dv  5663  mpt2eq3dva  5669  cbvmpt  5676  cbvmpt2x  5678  mpt2mptx  5708  ovmpt2x  5712  fmpt2x  5730  brtxp  5783  oqelins4  5794  brcrossg  5848  pw1fnf1o  5855  qseq2  5975  ecelqsg  5979  snec  5987  ecoptocl  5996  xpassen  6057  enpw1lem1  6061  enmap2lem3  6065  enmap1lem3  6071  enprmaplem5  6080  enprmapc  6083  1cnc  6139  df1c3g  6141  ncaddccl  6144  ncspw1eu  6159  pw1eltc  6162  el2c  6191  ce2  6192  dflec2  6210  lectr  6211  taddc  6229  tlecg  6230  letc  6231  ce0t  6232  nclenn  6249  csucex  6259  brcsuc  6260  addccan2nclem1  6263  addccan2nclem2  6264  ncslesuc  6267  nmembers1lem1  6268  nmembers1lem3  6270  nncdiv3lem1  6275  nncdiv3lem2  6276  nncdiv3  6277  nnc3n3p1  6278  spaccl  6286  spacind  6287  nchoicelem1  6289  nchoicelem2  6290  nchoicelem3  6291  nchoicelem11  6299  nchoicelem12  6300  nchoicelem16  6304  nchoicelem17  6305  frecsuc  6322
  Copyright terms: Public domain W3C validator