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

Theorem nfeq 2581
Description: Hypothesis builder for equality. (Contributed by NM, 21-Jun-1993.) (Revised 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 2432 . 2  |-  ( A  =  B  <->  A. z
( z  e.  A  <->  z  e.  B ) )
2 nfnfc.1 . . . . 5  |-  F/_ x A
32nfcri 2568 . . . 4  |-  F/ x  z  e.  A
4 nfeq.2 . . . . 5  |-  F/_ x B
54nfcri 2568 . . . 4  |-  F/ x  z  e.  B
63, 5nfbi 1866 . . 3  |-  F/ x
( z  e.  A  <->  z  e.  B )
76nfal 1872 . 2  |-  F/ x A. z ( z  e.  A  <->  z  e.  B
)
81, 7nfxfr 1615 1  |-  F/ x  A  =  B
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184   A.wal 1367    = wceq 1369   F/wnf 1589    e. wcel 1756   F/_wnfc 2561
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-cleq 2431  df-clel 2434  df-nfc 2563
This theorem is referenced by:  nfel  2582  nfeq1  2583  nfeq2  2585  nfne  2698  raleqf  2908  rexeqf  2909  reueq1f  2910  rmoeq1f  2911  rabeqf  2960  csbhypf  3302  sbceqg  3672  nffn  5502  nffo  5614  fvmptdf  5780  mpteqb  5783  fvmptf  5785  eqfnfv2f  5796  dff13f  5968  ovmpt2s  6209  ov2gf  6210  ovmpt2dxf  6211  ovmpt2df  6217  eqerlem  7125  seqof2  11856  sumeq2w  13161  sumeq2ii  13162  sumss  13193  fsumadd  13207  fsummulc2  13243  fsumrelem  13262  txcnp  19168  ptcnplem  19169  cnmpt11  19211  cnmpt21  19219  cnmptcom  19226  mbfeqalem  21095  mbflim  21121  itgeq1f  21224  itgeqa  21266  dvmptfsum  21422  ulmss  21837  leibpi  22312  o1cxp  22343  lgseisenlem2  22664  disjunsn  25887  opabdm  25894  opabrn  25895  mpt2mptxf  25946  f1od2  25975  fpwrelmap  25984  oms0  26662  prodeq1f  27372  prodeq2w  27376  prodeq2ii  27377  fprodmul  27422  fproddiv  27423  subtr  28462  subtr2  28463  iuneq2f  28920  mpt2bi123f  28928  mptbi12f  28932  dvdsrabdioph  29101  fphpd  29108  fvelrnbf  29693  refsum2cnlem1  29712  fmuldfeq  29717  climmulf  29730  climexp  29731  climsuse  29734  climrecf  29735  stoweidlem18  29766  stoweidlem31  29779  stoweidlem55  29803  stoweidlem59  29807  ovmpt2rdxf  30681  bnj1316  31701  bnj1446  31923  bnj1447  31924  bnj1448  31925  bnj1519  31943  bnj1520  31944  bnj1529  31948  bj-sbeqALT  32251
  Copyright terms: Public domain W3C validator