ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  nfeq Unicode version

Theorem nfeq 2266
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 2111 . 2  |-  ( A  =  B  <->  A. z
( z  e.  A  <->  z  e.  B ) )
2 nfnfc.1 . . . . 5  |-  F/_ x A
32nfcri 2252 . . . 4  |-  F/ x  z  e.  A
4 nfeq.2 . . . . 5  |-  F/_ x B
54nfcri 2252 . . . 4  |-  F/ x  z  e.  B
63, 5nfbi 1553 . . 3  |-  F/ x
( z  e.  A  <->  z  e.  B )
76nfal 1540 . 2  |-  F/ x A. z ( z  e.  A  <->  z  e.  B
)
81, 7nfxfr 1435 1  |-  F/ x  A  =  B
Colors of variables: wff set class
Syntax hints:    <-> wb 104   A.wal 1314    = wceq 1316   F/wnf 1421    e. wcel 1465   F/_wnfc 2245
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 683  ax-5 1408  ax-7 1409  ax-gen 1410  ax-ie1 1454  ax-ie2 1455  ax-8 1467  ax-10 1468  ax-11 1469  ax-i12 1470  ax-bndl 1471  ax-4 1472  ax-17 1491  ax-i9 1495  ax-ial 1499  ax-i5r 1500  ax-ext 2099
This theorem depends on definitions:  df-bi 116  df-tru 1319  df-nf 1422  df-sb 1721  df-cleq 2110  df-clel 2113  df-nfc 2247
This theorem is referenced by:  nfel  2267  nfeq1  2268  nfeq2  2270  nfne  2378  raleqf  2599  rexeqf  2600  reueq1f  2601  rmoeq1f  2602  rabeqf  2650  sbceqg  2989  csbhypf  3008  nfiotadxy  5061  nffn  5189  nffo  5314  fvmptdf  5476  mpteqb  5479  fvmptf  5481  eqfnfv2f  5490  dff13f  5639  ovmpos  5862  ov2gf  5863  ovmpodxf  5864  ovmpodf  5870  eqerlem  6428  sumeq2  11096  fsumadd  11143  txcnp  12367  cnmpt11  12379  cnmpt21  12387  cnmptcom  12394
  Copyright terms: Public domain W3C validator