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 2398 | . 2 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑)) | |
2 | nfa1 1506 | . 2 ⊢ Ⅎ𝑥∀𝑥(𝑥 ∈ 𝐴 → 𝜑) | |
3 | 1, 2 | nfxfr 1435 | 1 ⊢ Ⅎ𝑥∀𝑥 ∈ 𝐴 𝜑 |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∀wal 1314 Ⅎwnf 1421 ∈ wcel 1465 ∀wral 2393 |
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 1408 ax-gen 1410 ax-ial 1499 |
This theorem depends on definitions: df-bi 116 df-nf 1422 df-ral 2398 |
This theorem is referenced by: nfra2xy 2452 r19.12 2515 ralbi 2541 rexbi 2542 nfss 3060 ralidm 3433 nfii1 3814 dfiun2g 3815 mpteq12f 3978 reusv1 4349 ralxfrALT 4358 peano2 4479 fun11iun 5356 fvmptssdm 5473 ffnfv 5546 riota5f 5722 mpoeq123 5798 tfri3 6232 nfixp1 6580 nneneq 6719 exmidomni 6982 mkvprop 7000 caucvgsrlemgt1 7571 suplocsrlem 7584 lble 8673 indstr 9356 fimaxre2 10966 zsupcllemstep 11565 bezoutlemmain 11613 bezoutlemzz 11617 exmidunben 11866 mulcncf 12687 limccnp2cntop 12742 bj-rspgt 12920 isomninnlem 13152 |
Copyright terms: Public domain | W3C validator |