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

Theorem nfbi 1784
Description: If  x is not free in  ph and  ps, it is not free in  ( ph  <->  ps ). (Contributed by Mario Carneiro, 11-Aug-2016.)
Hypotheses
Ref Expression
nf.1  |-  F/ x ph
nf.2  |-  F/ x ps
Assertion
Ref Expression
nfbi  |-  F/ x
( ph  <->  ps )

Proof of Theorem nfbi
StepHypRef Expression
1 dfbi2 609 . 2  |-  ( (
ph 
<->  ps )  <->  ( ( ph  ->  ps )  /\  ( ps  ->  ph )
) )
2 nf.1 . . . 4  |-  F/ x ph
3 nf.2 . . . 4  |-  F/ x ps
42, 3nfim 1781 . . 3  |-  F/ x
( ph  ->  ps )
53, 2nfim 1781 . . 3  |-  F/ x
( ps  ->  ph )
64, 5nfan 1783 . 2  |-  F/ x
( ( ph  ->  ps )  /\  ( ps 
->  ph ) )
71, 6nfxfr 1560 1  |-  F/ x
( ph  <->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    /\ wa 358   F/wnf 1534
This theorem is referenced by:  euf  2162  sb8eu  2174  bm1.1  2281  abbi  2406  nfeq  2439  cleqf  2456  sbhypf  2846  ceqsexg  2912  elabgt  2924  elabgf  2925  axrep1  4148  axrep3  4150  axrep4  4151  copsex2t  4269  copsex2g  4270  opelopabsb  4291  opeliunxp2  4840  ralxpf  4846  cbviota  5240  sb8iota  5242  fmptco  5707  nfiso  5837  dfoprab4f  6194  fvopab5  6305  xpf1o  7039  zfcndrep  8252  uzindOLD  10122  gsumcom2  15242  isfildlem  17568  mbfsup  19035  mbfinf  19036  fmptcof2  23244  subtr2  26328  bnj1468  29194
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-11 1727
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-nf 1535
  Copyright terms: Public domain W3C validator