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

Theorem nfbi 1772
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 1769 . . 3  |-  F/ x
( ph  ->  ps )
53, 2nfim 1769 . . 3  |-  F/ x
( ps  ->  ph )
64, 5nfan 1771 . 2  |-  F/ x
( ( ph  ->  ps )  /\  ( ps 
->  ph ) )
71, 6nfxfr 1557 1  |-  F/ x
( ph  <->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    /\ wa 358   F/wnf 1531
This theorem is referenced by:  euf  2149  sb8eu  2161  bm1.1  2268  abbi  2393  nfeq  2426  cleqf  2443  sbhypf  2833  ceqsexg  2899  elabgt  2911  elabgf  2912  axrep1  4132  axrep3  4134  axrep4  4135  copsex2t  4253  copsex2g  4254  opelopabsb  4275  opeliunxp2  4824  ralxpf  4830  cbviota  5224  sb8iota  5226  fmptco  5691  nfiso  5821  dfoprab4f  6178  fvopab5  6289  xpf1o  7023  zfcndrep  8236  uzindOLD  10106  gsumcom2  15226  isfildlem  17552  mbfsup  19019  mbfinf  19020  fmptcof2  23229  subtr2  26225  bnj1468  28878
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-11 1715
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-nf 1532
  Copyright terms: Public domain W3C validator