MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  nfeq2 Structured version   Visualization version   GIF version

Theorem nfeq2 2999
Description: Hypothesis builder for equality, special case. (Contributed by Mario Carneiro, 10-Oct-2016.)
Hypothesis
Ref Expression
nfeq2.1 𝑥𝐵
Assertion
Ref Expression
nfeq2 𝑥 𝐴 = 𝐵
Distinct variable group:   𝑥,𝐴
Allowed substitution hint:   𝐵(𝑥)

Proof of Theorem nfeq2
StepHypRef Expression
1 nfcv 2982 . 2 𝑥𝐴
2 nfeq2.1 . 2 𝑥𝐵
31, 2nfeq 2995 1 𝑥 𝐴 = 𝐵
Colors of variables: wff setvar class
Syntax hints:   = wceq 1538  wnf 1785  wnfc 2962
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 1971  ax-7 2016  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2179  ax-ext 2796
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-tru 1541  df-ex 1782  df-nf 1786  df-cleq 2817  df-nfc 2964
This theorem is referenced by:  issetf  3493  eqvincf  3629  csbhypf  3894  nfpr  4613  intab  4892  nfmpt  5149  cbvmptf  5151  cbvmptfg  5152  zfrepclf  5184  eusvnf  5280  reusv2lem4  5289  reusv2  5291  moop2  5379  elrnmpt1  5817  opabiota  6737  fvmptdf  6765  fmptco  6882  elabrex  6994  nfmpo  7229  cbvmpox  7240  ovmpodxf  7293  zfrep6  7651  fmpox  7760  nfwrecs  7945  erovlem  8389  xpf1o  8676  mapxpen  8680  wdom2d  9041  cnfcom3clem  9165  scott0  9312  cplem2  9316  infxpenc2lem2  9444  acnlem  9472  fin23lem32  9764  hsmexlem2  9847  axcc3  9858  ac6num  9899  lble  11589  nfsum1  15046  nfsum  15047  nfsumOLD  15048  zsum  15075  fsum  15077  fsumcvg2  15084  fsum2dlem  15125  infcvgaux1i  15212  nfcprod1  15264  nfcprod  15265  zprod  15291  fprod  15295  fprodser  15303  fprod2dlem  15334  cayleyhamilton1  21504  neiptopreu  21745  xkocnv  22426  istrkg2ld  26261  cnlnadjlem5  29861  chirred  30185  iundisjf  30354  opabdm  30377  opabrn  30378  dfimafnf  30396  fmptcof2  30417  mpomptxf  30440  f1od2  30472  fpwrelmap  30484  fedgmullem2  31090  esum2dlem  31412  oms0  31616  bnj1468  32179  bnj981  32283  bnj1463  32388  satfv1  32671  iota5f  33016  nfwlim  33170  nffrecs  33181  bj-seex  34313  isbasisrelowllem1  34721  isbasisrelowllem2  34722  exrecfnlem  34745  finxpreclem6  34762  phpreu  34990  matunitlindflem2  35003  poimirlem24  35030  poimirlem25  35031  poimirlem26  35032  poimirlem27  35033  mbfposadd  35053  itg2addnclem  35057  cover2  35101  indexa  35120  riotasvd  36201  cdleme31sn1  37626  cdleme32fva  37682  cdlemk36  38158  elnn0rabdioph  39665  wdom2d2  39897  elabrexg  41600  cbvmpo2  41660  cbvmpo1  41661  dffo3f  41734  elrnmptf  41737  disjrnmpt2  41745  fmuldfeqlem1  42155  climf  42195  climf2  42239  cncficcgt0  42461  stoweidlem8  42581  stoweidlem16  42589  stoweidlem19  42592  stoweidlem21  42594  stoweidlem22  42595  stoweidlem23  42596  stoweidlem29  42602  stoweidlem32  42605  stoweidlem35  42608  stoweidlem36  42609  stoweidlem41  42614  stoweidlem44  42617  stoweidlem45  42618  stoweidlem51  42624  stoweidlem53  42626  stoweidlem60  42633  fourierdlem80  42759  sprsymrelf  43943  cbvmpox2  44668  ovmpordxf  44671  1arymaptfo  44988  2arymaptfo  44999
  Copyright terms: Public domain W3C validator