Description: Bound-variable hypothesis builder for restricted quantification. Version of nfral with a disjoint variable condition, which does not require ax-13 . (Contributed by NM, 1-Sep-1999) (Revised by Gino Giotto, 10-Jan-2024)
Ref | Expression | ||
---|---|---|---|
Hypotheses | nfralw.1 | |
|
nfralw.2 | |
||
Assertion | nfralw | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfralw.1 | |
|
2 | nfralw.2 | |
|
3 | nftru | |
|
4 | 1 | a1i | |
5 | 2 | a1i | |
6 | 3 4 5 | nfraldw | |
7 | 6 | mptru | |