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

Theorem nfeq 2531
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 2382 . 2  |-  ( A  =  B  <->  A. z
( z  e.  A  <->  z  e.  B ) )
2 nfnfc.1 . . . . 5  |-  F/_ x A
32nfcri 2518 . . . 4  |-  F/ x  z  e.  A
4 nfeq.2 . . . . 5  |-  F/_ x B
54nfcri 2518 . . . 4  |-  F/ x  z  e.  B
63, 5nfbi 1846 . . 3  |-  F/ x
( z  e.  A  <->  z  e.  B )
76nfal 1854 . 2  |-  F/ x A. z ( z  e.  A  <->  z  e.  B
)
81, 7nfxfr 1576 1  |-  F/ x  A  =  B
Colors of variables: wff set class
Syntax hints:    <-> wb 177   A.wal 1546   F/wnf 1550    = wceq 1649    e. wcel 1717   F/_wnfc 2511
This theorem is referenced by:  nfel  2532  nfeq1  2533  nfeq2  2535  nfne  2642  raleqf  2844  rexeqf  2845  reueq1f  2846  rmoeq1f  2847  rabeqf  2893  sbceqg  3211  csbhypf  3230  nffn  5482  nffo  5593  fvmptdf  5756  mpteqb  5759  fvmptf  5761  eqfnfv2f  5771  dff13f  5946  ovmpt2s  6137  ov2gf  6138  ovmpt2dxf  6139  ovmpt2df  6145  eqerlem  6874  seqof2  11309  sumeq1f  12410  sumeq2w  12414  sumeq2ii  12415  sumss  12446  fsumadd  12460  fsummulc2  12495  fsumrelem  12514  txcnp  17574  ptcnplem  17575  cnmpt11  17617  cnmpt21  17625  cnmptcom  17632  mbfeqalem  19402  mbflim  19428  itgeq1f  19531  itgeqa  19573  dvmptfsum  19727  ulmss  20181  leibpi  20650  o1cxp  20681  lgseisenlem2  21002  prodeq1f  25014  prodeq2w  25018  prodeq2ii  25019  fprodmul  25064  fproddiv  25065  subtr  26009  subtr2  26010  dvdsrabdioph  26562  fphpd  26569  fvelrnbf  27358  refsum2cnlem1  27377  fmuldfeq  27382  climmulf  27399  climexp  27400  climsuse  27403  climrecf  27404  stoweidlem18  27436  stoweidlem31  27449  stoweidlem55  27473  stoweidlem59  27477  bnj1316  28531  bnj1446  28753  bnj1447  28754  bnj1448  28755  bnj1519  28773  bnj1520  28774  bnj1529  28778
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2369
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-cleq 2381  df-clel 2384  df-nfc 2513
  Copyright terms: Public domain W3C validator