Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > nfra1 | GIF version |
Description: 𝑥 is not free in ∀𝑥 ∈ 𝐴𝜑. (Contributed by NM, 18-Oct-1996.) (Revised by Mario Carneiro, 7-Oct-2016.) |
Ref | Expression |
---|---|
nfra1 | ⊢ Ⅎ𝑥∀𝑥 ∈ 𝐴 𝜑 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-ral 2453 | . 2 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑)) | |
2 | nfa1 1534 | . 2 ⊢ Ⅎ𝑥∀𝑥(𝑥 ∈ 𝐴 → 𝜑) | |
3 | 1, 2 | nfxfr 1467 | 1 ⊢ Ⅎ𝑥∀𝑥 ∈ 𝐴 𝜑 |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∀wal 1346 Ⅎwnf 1453 ∈ wcel 2141 ∀wral 2448 |
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 1440 ax-gen 1442 ax-ial 1527 |
This theorem depends on definitions: df-bi 116 df-nf 1454 df-ral 2453 |
This theorem is referenced by: nfra2xy 2512 r19.12 2576 ralbi 2602 rexbi 2603 nfss 3140 ralidm 3515 nfii1 3904 dfiun2g 3905 mpteq12f 4069 reusv1 4443 ralxfrALT 4452 peano2 4579 fun11iun 5463 fvmptssdm 5580 ffnfv 5654 riota5f 5833 mpoeq123 5912 tfri3 6346 nfixp1 6696 nneneq 6835 exmidomni 7118 mkvprop 7134 caucvgsrlemgt1 7757 suplocsrlem 7770 lble 8863 indstr 9552 fimaxre2 11190 prodeq2 11520 zsupcllemstep 11900 bezoutlemmain 11953 bezoutlemzz 11957 exmidunben 12381 mulcncf 13385 limccnp2cntop 13440 bj-rspgt 13821 isomninnlem 14062 iswomninnlem 14081 ismkvnnlem 14084 |
Copyright terms: Public domain | W3C validator |