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

Theorem nfeq 2392
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 2247 . 2  |-  ( A  =  B  <->  A. z
( z  e.  A  <->  z  e.  B ) )
2 nfnfc.1 . . . . 5  |-  F/_ x A
32nfcri 2379 . . . 4  |-  F/ x  z  e.  A
4 nfeq.2 . . . . 5  |-  F/_ x B
54nfcri 2379 . . . 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 2372
This theorem is referenced by:  nfel  2393  nfeq1  2394  nfeq2  2396  nfne  2505  raleqf  2686  rexeqf  2687  reueq1f  2688  rabeqf  2720  sbceqg  3025  csbhypf  3044  nffn  5197  nffo  5307  fvmptdf  5463  mpteqb  5466  fvmptf  5468  eqfnfv2f  5478  dff13f  5636  ovmpt2s  5823  ov2gf  5824  ovmpt2dxf  5825  ovmpt2df  5831  opabiota  6177  eqerlem  6578  sumeq1f  12038  sumeq2w  12042  sumeq2ii  12043  sumss  12074  fsumadd  12088  fsummulc2  12123  fsumrelem  12142  txcnp  17146  ptcnplem  17147  cnmpt11  17189  cnmpt21  17197  cnmptcom  17204  mbfeqalem  18829  mbflim  18855  itgeq1f  18958  itgeqa  19000  dvmptfsum  19154  ulmss  19606  leibpi  20070  o1cxp  20101  lgseisenlem2  20421  prodeq3ii  24474  fprodadd  24518  fprodneg  24544  fprodsub  24545  subtr  25390  subtr2  25391  dvdsrabdioph  26057  fphpd  26065  bnj1316  27542  bnj1446  27764  bnj1447  27765  bnj1448  27766  bnj1519  27784  bnj1520  27785  bnj1529  27789
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 1926  ax-ext 2234
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 1883  df-cleq 2246  df-clel 2249  df-nfc 2374
  Copyright terms: Public domain W3C validator