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

Theorem nfal 1576
Description: If  x is not free in  ph, it is not free in  A. y ph. (Contributed by Mario Carneiro, 11-Aug-2016.) Remove dependency on ax-4 1510. (Revised by Gino Giotto, 25-Aug-2024.)
Hypothesis
Ref Expression
nfal.1  |-  F/ x ph
Assertion
Ref Expression
nfal  |-  F/ x A. y ph

Proof of Theorem nfal
StepHypRef Expression
1 df-nf 1461 . . . . . 6  |-  ( F/ x ph  <->  A. x
( ph  ->  A. x ph ) )
21biimpi 120 . . . . 5  |-  ( F/ x ph  ->  A. x
( ph  ->  A. x ph ) )
32alimi 1455 . . . 4  |-  ( A. y F/ x ph  ->  A. y A. x (
ph  ->  A. x ph )
)
4 ax-7 1448 . . . 4  |-  ( A. y A. x ( ph  ->  A. x ph )  ->  A. x A. y
( ph  ->  A. x ph ) )
5 ax-5 1447 . . . . . 6  |-  ( A. y ( ph  ->  A. x ph )  -> 
( A. y ph  ->  A. y A. x ph ) )
6 ax-7 1448 . . . . . 6  |-  ( A. y A. x ph  ->  A. x A. y ph )
75, 6syl6 33 . . . . 5  |-  ( A. y ( ph  ->  A. x ph )  -> 
( A. y ph  ->  A. x A. y ph ) )
87alimi 1455 . . . 4  |-  ( A. x A. y ( ph  ->  A. x ph )  ->  A. x ( A. y ph  ->  A. x A. y ph ) )
93, 4, 83syl 17 . . 3  |-  ( A. y F/ x ph  ->  A. x ( A. y ph  ->  A. x A. y ph ) )
10 df-nf 1461 . . 3  |-  ( F/ x A. y ph  <->  A. x ( A. y ph  ->  A. x A. y ph ) )
119, 10sylibr 134 . 2  |-  ( A. y F/ x ph  ->  F/ x A. y ph )
12 nfal.1 . 2  |-  F/ x ph
1311, 12mpg 1451 1  |-  F/ x A. y ph
Colors of variables: wff set class
Syntax hints:    -> wi 4   A.wal 1351   F/wnf 1460
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1447  ax-7 1448  ax-gen 1449
This theorem depends on definitions:  df-bi 117  df-nf 1461
This theorem is referenced by:  nfnf  1577  nfa2  1579  aaan  1587  cbv3  1742  cbv2  1749  nfald  1760  cbval2  1921  nfsb4t  2014  nfeuv  2044  mo23  2067  bm1.1  2162  nfnfc1  2322  nfnfc  2326  nfeq  2327  nfabdw  2338  sbcnestgf  3109  dfnfc2  3828  nfdisjv  3993  nfdisj1  3994  nffr  4350  exmidfodomrlemr  7201  exmidfodomrlemrALT  7202  exmidunben  12427  bdsepnft  14642  bdsepnfALT  14644  setindft  14720  strcollnft  14739  pw1nct  14755
  Copyright terms: Public domain W3C validator