![]() |
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 2422 | . 2 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑)) | |
2 | nfa1 1522 | . 2 ⊢ Ⅎ𝑥∀𝑥(𝑥 ∈ 𝐴 → 𝜑) | |
3 | 1, 2 | nfxfr 1451 | 1 ⊢ Ⅎ𝑥∀𝑥 ∈ 𝐴 𝜑 |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∀wal 1330 Ⅎwnf 1437 ∈ wcel 1481 ∀wral 2417 |
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 1424 ax-gen 1426 ax-ial 1515 |
This theorem depends on definitions: df-bi 116 df-nf 1438 df-ral 2422 |
This theorem is referenced by: nfra2xy 2478 r19.12 2541 ralbi 2567 rexbi 2568 nfss 3095 ralidm 3468 nfii1 3852 dfiun2g 3853 mpteq12f 4016 reusv1 4387 ralxfrALT 4396 peano2 4517 fun11iun 5396 fvmptssdm 5513 ffnfv 5586 riota5f 5762 mpoeq123 5838 tfri3 6272 nfixp1 6620 nneneq 6759 exmidomni 7022 mkvprop 7040 caucvgsrlemgt1 7627 suplocsrlem 7640 lble 8729 indstr 9415 fimaxre2 11030 prodeq2 11358 zsupcllemstep 11674 bezoutlemmain 11722 bezoutlemzz 11726 exmidunben 11975 mulcncf 12799 limccnp2cntop 12854 bj-rspgt 13164 isomninnlem 13400 iswomninnlem 13417 ismkvnnlem 13419 |
Copyright terms: Public domain | W3C validator |