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

Theorem nfbi 1857
Description: If  x is not free in  ph and  ps, it is not free in  ( ph  <->  ps ). (Contributed by Mario Carneiro, 11-Aug-2016.) (Proof shortened by Wolf Lammen, 2-Jan-2018.)
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 nf.1 . . . 4  |-  F/ x ph
21a1i 11 . . 3  |-  (  T. 
->  F/ x ph )
3 nf.2 . . . 4  |-  F/ x ps
43a1i 11 . . 3  |-  (  T. 
->  F/ x ps )
52, 4nfbid 1855 . 2  |-  (  T. 
->  F/ x ( ph  <->  ps ) )
65trud 1333 1  |-  F/ x
( ph  <->  ps )
Colors of variables: wff set class
Syntax hints:    <-> wb 178    T. wtru 1326   F/wnf 1554
This theorem is referenced by:  euf  2289  sb8eu  2301  bm1.1  2423  abbi  2548  nfeq  2581  cleqf  2598  sbhypf  3003  ceqsexg  3069  elabgt  3081  elabgf  3082  axrep1  4324  axrep3  4326  axrep4  4327  copsex2t  4446  copsex2g  4447  opelopabsb  4468  opeliunxp2  5016  ralxpf  5022  cbviota  5426  sb8iota  5428  fmptco  5904  nfiso  6047  dfoprab4f  6408  fvopab5  6537  xpf1o  7272  zfcndrep  8494  uzindOLD  10369  gsumcom2  15554  isfildlem  17894  cnextfvval  18101  mbfsup  19559  mbfinf  19560  fmptcof2  24081  subtr2  26332  bnj1468  29291
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-11 1762
This theorem depends on definitions:  df-bi 179  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555
  Copyright terms: Public domain W3C validator