![]() |
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 2375 | . 2 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑)) | |
2 | nfa1 1486 | . 2 ⊢ Ⅎ𝑥∀𝑥(𝑥 ∈ 𝐴 → 𝜑) | |
3 | 1, 2 | nfxfr 1415 | 1 ⊢ Ⅎ𝑥∀𝑥 ∈ 𝐴 𝜑 |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∀wal 1294 Ⅎwnf 1401 ∈ wcel 1445 ∀wral 2370 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-5 1388 ax-gen 1390 ax-ial 1479 |
This theorem depends on definitions: df-bi 116 df-nf 1402 df-ral 2375 |
This theorem is referenced by: nfra2xy 2429 r19.12 2491 ralbi 2515 rexbi 2516 nfss 3032 ralidm 3402 nfii1 3783 dfiun2g 3784 mpteq12f 3940 reusv1 4308 ralxfrALT 4317 peano2 4438 fun11iun 5309 fvmptssdm 5423 ffnfv 5495 riota5f 5670 mpt2eq123 5746 tfri3 6170 nfixp1 6515 nneneq 6653 exmidomni 6885 mkvprop 6901 caucvgsrlemgt1 7437 lble 8505 indstr 9180 fimaxre2 10773 zsupcllemstep 11368 bezoutlemmain 11414 bezoutlemzz 11418 mulcncf 12354 bj-rspgt 12394 |
Copyright terms: Public domain | W3C validator |