![]() |
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 2470 | . 2 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑)) | |
2 | nfa1 1551 | . 2 ⊢ Ⅎ𝑥∀𝑥(𝑥 ∈ 𝐴 → 𝜑) | |
3 | 1, 2 | nfxfr 1484 | 1 ⊢ Ⅎ𝑥∀𝑥 ∈ 𝐴 𝜑 |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∀wal 1361 Ⅎwnf 1470 ∈ wcel 2158 ∀wral 2465 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-5 1457 ax-gen 1459 ax-ial 1544 |
This theorem depends on definitions: df-bi 117 df-nf 1471 df-ral 2470 |
This theorem is referenced by: nfra2xy 2529 r19.12 2593 ralbi 2619 rexbi 2620 nfss 3160 ralidm 3535 nfii1 3929 dfiun2g 3930 mpteq12f 4095 reusv1 4470 ralxfrALT 4479 peano2 4606 fun11iun 5494 fvmptssdm 5613 ffnfv 5687 riota5f 5868 mpoeq123 5947 tfri3 6382 nfixp1 6732 nneneq 6871 exmidomni 7154 mkvprop 7170 caucvgsrlemgt1 7808 suplocsrlem 7821 lble 8918 indstr 9607 fimaxre2 11249 prodeq2 11579 zsupcllemstep 11960 bezoutlemmain 12013 bezoutlemzz 12017 exmidunben 12441 mulcncf 14444 limccnp2cntop 14499 bj-rspgt 14891 isomninnlem 15132 iswomninnlem 15151 ismkvnnlem 15154 |
Copyright terms: Public domain | W3C validator |