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

Theorem nfeq 2509
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 2360 . 2  |-  ( A  =  B  <->  A. z
( z  e.  A  <->  z  e.  B ) )
2 nfnfc.1 . . . . 5  |-  F/_ x A
32nfcri 2496 . . . 4  |-  F/ x  z  e.  A
4 nfeq.2 . . . . 5  |-  F/_ x B
54nfcri 2496 . . . 4  |-  F/ x  z  e.  B
63, 5nfbi 1844 . . 3  |-  F/ x
( z  e.  A  <->  z  e.  B )
76nfal 1852 . 2  |-  F/ x A. z ( z  e.  A  <->  z  e.  B
)
81, 7nfxfr 1575 1  |-  F/ x  A  =  B
Colors of variables: wff set class
Syntax hints:    <-> wb 176   A.wal 1545   F/wnf 1549    = wceq 1647    e. wcel 1715   F/_wnfc 2489
This theorem is referenced by:  nfel  2510  nfeq1  2511  nfeq2  2513  nfne  2620  raleqf  2817  rexeqf  2818  reueq1f  2819  rmoeq1f  2820  rabeqf  2866  sbceqg  3183  csbhypf  3202  nffn  5445  nffo  5556  fvmptdf  5718  mpteqb  5721  fvmptf  5723  eqfnfv2f  5733  dff13f  5906  ovmpt2s  6097  ov2gf  6098  ovmpt2dxf  6099  ovmpt2df  6105  opabiota  6435  eqerlem  6834  seqof2  11268  sumeq1f  12369  sumeq2w  12373  sumeq2ii  12374  sumss  12405  fsumadd  12419  fsummulc2  12454  fsumrelem  12473  txcnp  17531  ptcnplem  17532  cnmpt11  17574  cnmpt21  17582  cnmptcom  17589  mbfeqalem  19212  mbflim  19238  itgeq1f  19341  itgeqa  19383  dvmptfsum  19537  ulmss  19991  leibpi  20460  o1cxp  20491  lgseisenlem2  20812  disjabrex  23422  disjabrexf  23423  iundisjf  23426  dfimafnf  23446  neiptopreu  23645  voliune  24048  volfiniune  24049  prodeq1f  24718  prodeq2w  24722  prodeq2ii  24723  fprodmul  24768  fproddiv  24769  subtr  25731  subtr2  25732  dvdsrabdioph  26397  fphpd  26405  fvelrnbf  27195  refsum2cnlem1  27214  fmuldfeqlem1  27218  fmuldfeq  27219  climmulf  27236  climexp  27237  climsuse  27240  climrecf  27241  stoweidlem8  27263  stoweidlem16  27271  stoweidlem18  27273  stoweidlem19  27274  stoweidlem21  27276  stoweidlem22  27277  stoweidlem23  27278  stoweidlem28  27283  stoweidlem29  27284  stoweidlem31  27286  stoweidlem32  27287  stoweidlem35  27290  stoweidlem36  27291  stoweidlem41  27296  stoweidlem44  27299  stoweidlem45  27300  stoweidlem48  27303  stoweidlem51  27306  stoweidlem53  27308  stoweidlem55  27310  stoweidlem58  27313  stoweidlem59  27314  stoweidlem60  27315  bnj1316  28617  bnj1446  28839  bnj1447  28840  bnj1448  28841  bnj1519  28859  bnj1520  28860  bnj1529  28864
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1551  ax-5 1562  ax-17 1621  ax-9 1659  ax-8 1680  ax-6 1734  ax-7 1739  ax-11 1751  ax-12 1937  ax-ext 2347
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1324  df-ex 1547  df-nf 1550  df-sb 1654  df-cleq 2359  df-clel 2362  df-nfc 2491
  Copyright terms: Public domain W3C validator