Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > nfbi | Unicode version |
Description: If is not free in and , then it is not free in . (Contributed by Mario Carneiro, 11-Aug-2016.) (Proof shortened by Wolf Lammen, 2-Jan-2018.) |
Ref | Expression |
---|---|
nfbi.1 | |
nfbi.2 |
Ref | Expression |
---|---|
nfbi |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfbi.1 | . . . 4 | |
2 | 1 | a1i 9 | . . 3 |
3 | nfbi.2 | . . . 4 | |
4 | 3 | a1i 9 | . . 3 |
5 | 2, 4 | nfbid 1552 | . 2 |
6 | 5 | mptru 1325 | 1 |
Colors of variables: wff set class |
Syntax hints: wb 104 wtru 1317 wnf 1421 |
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-5 1408 ax-gen 1410 ax-4 1472 ax-ial 1499 ax-i5r 1500 |
This theorem depends on definitions: df-bi 116 df-tru 1319 df-nf 1422 |
This theorem is referenced by: sb8eu 1990 nfeuv 1995 bm1.1 2102 abbi 2231 nfeq 2266 cleqf 2282 sbhypf 2709 ceqsexg 2787 elabgt 2799 elabgf 2800 copsex2t 4137 copsex2g 4138 opelopabsb 4152 opeliunxp2 4649 ralxpf 4655 rexxpf 4656 cbviota 5063 sb8iota 5065 fmptco 5554 nfiso 5675 dfoprab4f 6059 opeliunxp2f 6103 xpf1o 6706 bdsepnfALT 13014 strcollnfALT 13111 |
Copyright terms: Public domain | W3C validator |