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

Theorem nfeq 2426
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
Dummy variable  z is distinct from all other variables.
StepHypRef Expression
1 dfcleq 2277 . 2  |-  ( A  =  B  <->  A. z
( z  e.  A  <->  z  e.  B ) )
2 nfnfc.1 . . . . 5  |-  F/_ x A
32nfcri 2413 . . . 4  |-  F/ x  z  e.  A
4 nfeq.2 . . . . 5  |-  F/_ x B
54nfcri 2413 . . . 4  |-  F/ x  z  e.  B
63, 5nfbi 1772 . . 3  |-  F/ x
( z  e.  A  <->  z  e.  B )
76nfal 1766 . 2  |-  F/ x A. z ( z  e.  A  <->  z  e.  B
)
81, 7nfxfr 1557 1  |-  F/ x  A  =  B
Colors of variables: wff set class
Syntax hints:    <-> wb 176   A.wal 1527   F/wnf 1531    = wceq 1623    e. wcel 1684   F/_wnfc 2406
This theorem is referenced by:  nfel  2427  nfeq1  2428  nfeq2  2430  nfne  2539  raleqf  2732  rexeqf  2733  reueq1f  2734  rmoeq1f  2735  rabeqf  2781  sbceqg  3097  csbhypf  3116  nffn  5340  nffo  5450  fvmptdf  5611  mpteqb  5614  fvmptf  5616  eqfnfv2f  5626  dff13f  5784  ovmpt2s  5971  ov2gf  5972  ovmpt2dxf  5973  ovmpt2df  5979  opabiota  6293  eqerlem  6692  sumeq1f  12161  sumeq2w  12165  sumeq2ii  12166  sumss  12197  fsumadd  12211  fsummulc2  12246  fsumrelem  12265  txcnp  17314  ptcnplem  17315  cnmpt11  17357  cnmpt21  17365  cnmptcom  17372  mbfeqalem  18997  mbflim  19023  itgeq1f  19126  itgeqa  19168  dvmptfsum  19322  ulmss  19774  leibpi  20238  o1cxp  20269  lgseisenlem2  20589  dfimafnf  23041  disjabrex  23359  disjabrexf  23360  iundisjf  23365  prodeq3ii  25308  fprodadd  25352  fprodneg  25378  fprodsub  25379  subtr  26224  subtr2  26225  dvdsrabdioph  26891  fphpd  26899  fvelrnbf  27689  refsum2cnlem1  27708  fmuldfeqlem1  27712  fmuldfeq  27713  climmulf  27730  climexp  27731  climsuse  27734  climrecf  27735  stoweidlem8  27757  stoweidlem16  27765  stoweidlem18  27767  stoweidlem19  27768  stoweidlem21  27770  stoweidlem22  27771  stoweidlem23  27772  stoweidlem28  27777  stoweidlem29  27778  stoweidlem31  27780  stoweidlem32  27781  stoweidlem35  27784  stoweidlem36  27785  stoweidlem41  27790  stoweidlem44  27793  stoweidlem45  27794  stoweidlem48  27797  stoweidlem51  27800  stoweidlem53  27802  stoweidlem55  27804  stoweidlem58  27807  stoweidlem59  27808  stoweidlem60  27809  bnj1316  28853  bnj1446  29075  bnj1447  29076  bnj1448  29077  bnj1519  29095  bnj1520  29096  bnj1529  29100
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