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

Theorem nfeq 2399
Description: Hypothesis builder for equality. (Contributed by Mario Carneiro, 11-Aug-2016.)
Hypotheses
Ref Expression
nfnfc.1  |-  F/_ x A
nfeq.2  |-  F/_ x B
Assertion
Ref Expression
nfeq  |-  F/ x  A  =  B

Proof of Theorem nfeq
StepHypRef Expression
1 dfcleq 2250 . 2  |-  ( A  =  B  <->  A. z
( z  e.  A  <->  z  e.  B ) )
2 nfnfc.1 . . . . 5  |-  F/_ x A
32nfcri 2386 . . . 4  |-  F/ x  z  e.  A
4 nfeq.2 . . . . 5  |-  F/_ x B
54nfcri 2386 . . . 4  |-  F/ x  z  e.  B
63, 5nfbi 1738 . . 3  |-  F/ x
( z  e.  A  <->  z  e.  B )
76nfal 1732 . 2  |-  F/ x A. z ( z  e.  A  <->  z  e.  B
)
81, 7nfxfr 1562 1  |-  F/ x  A  =  B
Colors of variables: wff set class
Syntax hints:    <-> wb 178   A.wal 1532   F/wnf 1539    = wceq 1619    e. wcel 1621   F/_wnfc 2379
This theorem is referenced by:  nfel  2400  nfeq1  2401  nfeq2  2403  nfne  2512  raleqf  2695  rexeqf  2696  reueq1f  2697  rabeqf  2733  sbceqg  3039  csbhypf  3058  nffn  5243  nffo  5353  fvmptdf  5510  mpteqb  5513  fvmptf  5515  eqfnfv2f  5525  dff13f  5683  ovmpt2s  5870  ov2gf  5871  ovmpt2dxf  5872  ovmpt2df  5878  opabiota  6224  eqerlem  6625  sumeq1f  12091  sumeq2w  12095  sumeq2ii  12096  sumss  12127  fsumadd  12141  fsummulc2  12176  fsumrelem  12195  txcnp  17241  ptcnplem  17242  cnmpt11  17284  cnmpt21  17292  cnmptcom  17299  mbfeqalem  18924  mbflim  18950  itgeq1f  19053  itgeqa  19095  dvmptfsum  19249  ulmss  19701  leibpi  20165  o1cxp  20196  lgseisenlem2  20516  dfimafnf  22967  prodeq3ii  24640  fprodadd  24684  fprodneg  24710  fprodsub  24711  subtr  25556  subtr2  25557  dvdsrabdioph  26223  fphpd  26231  fvelrnbf  27022  refsum2cnlem1  27041  fmuldfeqlem1  27045  fmuldfeq  27046  stoweidlem8  27057  stoweidlem16  27065  stoweidlem18  27067  stoweidlem19  27068  stoweidlem21  27070  stoweidlem22  27071  stoweidlem23  27072  stoweidlem28  27077  stoweidlem29  27078  stoweidlem31  27080  stoweidlem32  27081  stoweidlem35  27084  stoweidlem36  27085  stoweidlem41  27090  stoweidlem44  27093  stoweidlem45  27094  stoweidlem48  27097  stoweidlem51  27100  stoweidlem53  27102  stoweidlem55  27104  stoweidlem58  27107  stoweidlem59  27108  stoweidlem60  27109  bnj1316  27865  bnj1446  28087  bnj1447  28088  bnj1448  28089  bnj1519  28107  bnj1520  28108  bnj1529  28112
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1927  ax-ext 2237
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1884  df-cleq 2249  df-clel 2252  df-nfc 2381
  Copyright terms: Public domain W3C validator