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

Theorem nfeq2 2430
Description: Hypothesis builder for equality, special case. (Contributed by Mario Carneiro, 10-Oct-2016.)
Hypothesis
Ref Expression
nfeq2.1  |-  F/_ x B
Assertion
Ref Expression
nfeq2  |-  F/ x  A  =  B
Distinct variable group:    x, A
Allowed substitution hint:    B( x)

Proof of Theorem nfeq2
StepHypRef Expression
1 nfcv 2419 . 2  |-  F/_ x A
2 nfeq2.1 . 2  |-  F/_ x B
31, 2nfeq 2426 1  |-  F/ x  A  =  B
Colors of variables: wff set class
Syntax hints:   F/wnf 1531    = wceq 1623   F/_wnfc 2406
This theorem is referenced by:  issetf  2793  eqvincf  2896  csbhypf  3116  nfpr  3680  intab  3892  nfmpt  4108  cbvmpt  4110  zfrepclf  4137  moop2  4261  eusvnf  4529  reusv2lem4  4538  reusv2  4540  elrnmpt1  4928  fmptco  5691  zfrep6  5748  elabrex  5765  nfmpt2  5916  cbvmpt2x  5924  ovmpt2dxf  5973  fmpt2x  6190  riotasvd  6347  nfrecs  6390  erovlem  6754  xpf1o  7023  mapxpen  7027  wdom2d  7294  cnfcom3clem  7408  scott0  7556  cplem2  7560  infxpenc2lem2  7647  acnlem  7675  fin23lem32  7970  hsmexlem2  8053  axcc3  8064  ac6num  8106  lble  9706  nfsum1  12163  nfsum  12164  fsum  12193  fsumcvg2  12200  fsum2dlem  12233  infcvgaux1i  12315  xkocnv  17505  cnlnadjlem5  22651  chirred  22975  cbvmptf  23220  fmptcof2  23229  svli2  25484  intopcoaconb  25540  cnegvex2  25660  rnegvex2  25661  cover2  26358  indexa  26412  elnn0rabdioph  26884  wdom2d2  27128  bnj1468  28878  bnj981  28982  bnj1463  29085  cdleme31sn1  30570  cdleme32fva  30626  cdlemk36  31102
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-cleq 2276  df-clel 2279  df-nfc 2408
  Copyright terms: Public domain W3C validator