Theorem nfeq 2776

Description: Hypothesis builder for equality. (Contributed by NM, 21-Jun-1993.) (Revised by Mario Carneiro, 11-Aug-2016.) (Proof shortened by Wolf Lammen, 16-Nov-2019.)

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

Step	Hyp	Ref	Expression
1		nfnfc.1	. . . 4 |- F/_ x A
2	1	a1i 11	. . 3 |- ( T. -> F/_ x A )
3		nfeq.2	. . . 4 |- F/_ x B
4	3	a1i 11	. . 3 |- ( T. -> F/_ x B )
5	2, 4	nfeqd 2772	. 2 |- ( T. -> F/ x A = B )
6	5	trud 1493	1 |- F/ x A = B

Syntax hints:   = wceq 1483   T. wtru 1484   F/wnf 1708   F/_wnfc 2751

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-cleq 2615  df-nfc 2753

This theorem is referenced by:  nfeq1  2778  nfeq2  2780  nfne  2894  raleqf  3134  rexeqf  3135  reueq1f  3136  rmoeq1f  3137  rabeqf  3190  csbhypf  3552  sbceqg  3984  nffn  5987  nffo  6114  fvmptd3f  6295  mpteqb  6299  fvmptf  6301  eqfnfv2f  6315  dff13f  6513  ovmpt2s  6784  ov2gf  6785  ovmpt2dxf  6786  ovmpt2df  6792  eqerlem  7776  seqof2  12859  sumeq2ii  14423  sumss  14455  fsumadd  14470  fsummulc2  14516  fsumrelem  14539  prodeq1f  14638  prodeq2ii  14643  fprodmul  14690  fproddiv  14691  fprodle  14727  txcnp  21423  ptcnplem  21424  cnmpt11  21466  cnmpt21  21474  cnmptcom  21481  mbfeqalem  23409  mbflim  23435  itgeq1f  23538  itgeqa  23580  dvmptfsum  23738  ulmss  24151  leibpi  24669  o1cxp  24701  lgseisenlem2  25101  fmptcof2  29457  aciunf1lem  29462  sigapildsys  30225  bnj1316  30891  bnj1446  31113  bnj1447  31114  bnj1448  31115  bnj1519  31133  bnj1520  31134  bnj1529  31138  nosupbnd1  31860  subtr  32308  subtr2  32309  bj-sbeqALT  32895  poimirlem25  33434  iuneq2f  33963  mpt2bi123f  33971  mptbi12f  33975  dvdsrabdioph  37374  fphpd  37380  fvelrnbf  39177  refsum2cnlem1  39196  dffo3f  39364  elrnmptf  39367  disjrnmpt2  39375  disjinfi  39380  choicefi  39392  axccdom  39416  fvelimad  39458  uzublem  39657  fsumf1of  39806  fmuldfeq  39815  mccl  39830  climmulf  39836  climexp  39837  climsuse  39840  climrecf  39841  climaddf  39847  mullimc  39848  neglimc  39879  addlimc  39880  0ellimcdiv  39881  climeldmeqmpt  39900  climfveqmpt  39903  climfveqf  39912  climfveqmpt3  39914  climeldmeqf  39915  climeqf  39920  climeldmeqmpt3  39921  limsupubuzlem  39944  limsupequz  39955  dvnmptdivc  40153  dvmptfprod  40160  dvnprodlem1  40161  stoweidlem18  40235  stoweidlem31  40248  stoweidlem55  40272  stoweidlem59  40276  sge0f1o  40599  sge0iunmpt  40635  sge0reuz  40664  iundjiun  40677  hoicvrrex  40770  ovnhoilem1  40815  ovnlecvr2  40824  opnvonmbllem1  40846  vonioo  40896  vonicc  40899  sssmf  40947  smflim  40985  smfpimcclem  41013  smfpimcc  41014  ovmpt2rdxf  42117