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 3514 nfii1 3902 dfiun2g 3903 mpteq12f 4067 reusv1 4441 ralxfrALT 4450 peano2 4577 fun11iun 5461 fvmptssdm 5578 ffnfv 5651 riota5f 5830 mpoeq123 5909 tfri3 6343 nfixp1 6692 nneneq 6831 exmidomni 7114 mkvprop 7130 caucvgsrlemgt1 7744 suplocsrlem 7757 lble 8850 indstr 9539 fimaxre2 11177 prodeq2 11507 zsupcllemstep 11887 bezoutlemmain 11940 bezoutlemzz 11944 exmidunben 12368 mulcncf 13344 limccnp2cntop 13399 bj-rspgt 13780 isomninnlem 14022 iswomninnlem 14041 ismkvnnlem 14044 |
Copyright terms: Public domain | W3C validator |